no goals
R : Type u_1
inst✝⁴ : StrictOrderedCommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type ?u.10058
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_3
⊢ map ι (LinearEquiv.refl R M) = Equiv.refl (Orientation R M ι)
rw [Orientation.map, AlternatingMap.domLCongr_refl, Module.Ray.map_refl]