-- Mathlib/LinearAlgebra/Orientation.lean
theorem map_orientation_eq_det_inv_smul [Finite ι] (e : Basis ι R M) (x : Orientation R M ι)
    (f : M ≃ₗ[R] M) : Orientation.map ι f x = (LinearEquiv.det f)⁻¹ • x

Proof state:
case intro.h
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ (Orientation.map ι f) (rayOfNeZero R g hg) = (LinearEquiv.det f)⁻¹ • rayOfNeZero R g hg

Tactic:
rw [Orientation.map_apply, smul_rayOfNeZero, ray_eq_iff, Units.smul_def,
  (g.compLinearMap f.symm).eq_smul_basis_det e, g.eq_smul_basis_det e,
  AlternatingMap.compLinearMap_apply, AlternatingMap.smul_apply,
  show (fun i ↦ (LinearEquiv.symm f).toLinearMap (e i)) = (LinearEquiv.symm f).toLinearMap ∘ e
  by rfl, Basis.det_comp, Basis.det_self, mul_one, smul_eq_mul, mul_comm, mul_smul,
  LinearEquiv.coe_inv_det]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
⊢ (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
val✝ : Fintype ι
⊢ (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x

Proof state:
case intro
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x

Tactic:
induction x using Module.Ray.ind with | h g hg =>
rw [Orientation.map_apply, smul_rayOfNeZero, ray_eq_iff, Units.smul_def,
  (g.compLinearMap f.symm).eq_smul_basis_det e, g.eq_smul_basis_det e,
  AlternatingMap.compLinearMap_apply, AlternatingMap.smul_apply,
  show (fun i ↦ (LinearEquiv.symm f).toLinearMap (e i)) = (LinearEquiv.symm f).toLinearMap ∘ e
  by rfl, Basis.det_comp, Basis.det_self, mul_one, smul_eq_mul, mul_comm, mul_smul,
  LinearEquiv.coe_inv_det]

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
val✝ : Fintype ι
⊢ (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x

Tactic:
letI := Classical.decEq ι

Result:
case intro
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
x : Orientation R M ι
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ (fun i => ↑f.symm (e i)) = ⇑↑f.symm ∘ ⇑e

Tactic:
rfl

Result:
no goals