-- Mathlib/LinearAlgebra/Orientation.lean
theorem Orientation.map_of_isEmpty [IsEmpty ι] (x : Orientation R M ι) (f : M ≃ₗ[R] M) :
    Orientation.map ι f x = x

Proof state:
case h.e_v.H
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
⊢ (g fun i_1 => ↑f.symm (i i_1)) = g i

Tactic:
congr

Result:
case h.e_v.H.h.e_6.h
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
⊢ (fun i_1 => ↑f.symm (i i_1)) = i

Proof state:
case h.e_v.H.h.e_6.h
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
⊢ (fun i_1 => ↑f.symm (i i_1)) = i

Tactic:
simp only [LinearEquiv.coe_coe, eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case h.e_v
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ g.compLinearMap ↑f.symm = g

Tactic:
ext i

Result:
case h.e_v.H
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
⊢ (g.compLinearMap ↑f.symm) i = g i

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
x : Orientation R M ι
f : M ≃ₗ[R] M
⊢ (map ι f) x = x

Tactic:
induction x using Module.Ray.ind with | h g hg =>
rw [Orientation.map_apply]
congr
ext i
rw [AlternatingMap.compLinearMap_apply]
congr
simp only [LinearEquiv.coe_coe, eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case h.e_v.H
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
⊢ (g.compLinearMap ↑f.symm) i = g i

Tactic:
rw [AlternatingMap.compLinearMap_apply]

Result:
case h.e_v.H
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
⊢ (g fun i_1 => ↑f.symm (i i_1)) = g i

Proof state:
case h
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ (map ι f) (rayOfNeZero R g hg) = rayOfNeZero R g hg

Tactic:
rw [Orientation.map_apply]

Result:
case h
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ rayOfNeZero R (g.compLinearMap ↑f.symm) ⋯ = rayOfNeZero R g hg

Proof state:
case h
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ rayOfNeZero R (g.compLinearMap ↑f.symm) ⋯ = rayOfNeZero R g hg

Tactic:
congr

Result:
case h.e_v
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ g.compLinearMap ↑f.symm = g