case h
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ ↑(map ι f) (rayOfNeZero R g hg) = rayOfNeZero R g hg
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
x : Orientation R M ι
f : M ≃ₗ[R] M
⊢ ↑(map ι f) x = x
induction' x using Module.Ray.ind with g hg
case h
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ rayOfNeZero R (AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f))
      (_ : ¬AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f) = 0) =
    rayOfNeZero R g hg
case h
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ ↑(map ι f) (rayOfNeZero R g hg) = rayOfNeZero R g hg
rw [Orientation.map_apply]
case h.e_v
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f) = g
case h
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ rayOfNeZero R (AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f))
      (_ : ¬AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f) = 0) =
    rayOfNeZero R g hg
congr
case h.e_v.H
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
i : ι → M
⊢ ↑(AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f)) i = ↑g i
case h.e_v
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
⊢ AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f) = g
ext i
case h.e_v.H
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
i : ι → M
⊢ (↑g fun i_1 => ↑↑(LinearEquiv.symm f) (i i_1)) = ↑g i
case h.e_v.H
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
i : ι → M
⊢ ↑(AlternatingMap.compLinearMap g ↑(LinearEquiv.symm f)) i = ↑g i
rw [AlternatingMap.compLinearMap_apply]
case h.e_v.H.h.e_6.h
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
i : ι → M
⊢ (fun i_1 => ↑↑(LinearEquiv.symm f) (i i_1)) = i
case h.e_v.H
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
i : ι → M
⊢ (↑g fun i_1 => ↑↑(LinearEquiv.symm f) (i i_1)) = ↑g i
congr
no goals
case h.e_v.H.h.e_6.h
R : Type u_2
inst✝⁵ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type ?u.31631
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : AlternatingMap R M R ι
hg : g ≠ 0
i : ι → M
⊢ (fun i_1 => ↑↑(LinearEquiv.symm f) (i i_1)) = i
simp only [LinearEquiv.coe_coe, eq_iff_true_of_subsingleton]