-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_conj {N : Type*} [AddCommGroup N] [Module A N] (f : M →ₗ[A] M) (e : M ≃ₗ[A] N) :
    LinearMap.det ((e : M →ₗ[A] N) ∘ₗ f ∘ₗ (e.symm : N →ₗ[A] M)) = LinearMap.det f

Proof state:
case neg
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
have H' : ¬∃ t : Finset N, Nonempty (Basis t A N) := by
  contrapose! H
  rcases H with ⟨s, ⟨b⟩⟩
  exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩

Result:
case neg
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
H' : ¬∃ t, Nonempty (Basis { x // x ∈ t } A N)
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ∃ t, Nonempty (Basis { x // x ∈ t } A N)
⊢ ∃ s, Nonempty (Basis { x // x ∈ s } A M)

Tactic:
rcases H with ⟨s, ⟨b⟩⟩

Result:
case intro.intro
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset N
b : Basis { x // x ∈ s } A N
⊢ ∃ s, Nonempty (Basis { x // x ∈ s } A M)

Proof state:
case pos.intro.intro.hM'M
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis { x // x ∈ s } A M
⊢ (toMatrix (b.map e) b) ↑e.symm * (toMatrix b (b.map e)) ↑e = 1

Tactic:
rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
  toMatrix_id]

Result:
no goals

Proof state:
case intro.intro
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset N
b : Basis { x // x ∈ s } A N
⊢ ∃ s, Nonempty (Basis { x // x ∈ s } A M)

Tactic:
exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩

Result:
no goals

Proof state:
case pos.intro.intro
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis { x // x ∈ s } A M
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
rw [← det_toMatrix b f, ← det_toMatrix (b.map e), toMatrix_comp (b.map e) b (b.map e),
  toMatrix_comp (b.map e) b b, ← Matrix.mul_assoc, Matrix.det_conj_of_mul_eq_one]

Result:
case pos.intro.intro.hMM'
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis { x // x ∈ s } A M
⊢ (toMatrix b (b.map e)) ↑e * (toMatrix (b.map e) b) ↑e.symm = 1

case pos.intro.intro.hM'M
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis { x // x ∈ s } A M
⊢ (toMatrix (b.map e) b) ↑e.symm * (toMatrix b (b.map e)) ↑e = 1

Proof state:
case neg
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
H' : ¬∃ t, Nonempty (Basis { x // x ∈ t } A N)
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg, not_false_eq_true]

Result:
no goals

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ ¬∃ t, Nonempty (Basis { x // x ∈ t } A N)

Tactic:
contrapose! H

Result:
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ∃ t, Nonempty (Basis { x // x ∈ t } A N)
⊢ ∃ s, Nonempty (Basis { x // x ∈ s } A M)

Proof state:
case pos.intro.intro.hMM'
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis { x // x ∈ s } A M
⊢ (toMatrix b (b.map e)) ↑e * (toMatrix (b.map e) b) ↑e.symm = 1

Tactic:
rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
  toMatrix_id]

Result:
no goals

Proof state:
case pos
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
rcases H with ⟨s, ⟨b⟩⟩

Result:
case pos.intro.intro
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis { x // x ∈ s } A M
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)

Result:
case pos
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

case neg
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f