case pos
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (comp (↑e) (comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f

case neg
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (comp (↑e) (comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
⊢ ↑LinearMap.det (comp (↑e) (comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f
by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
case pos.intro.intro
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (comp (↑e) (comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f
case pos
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (comp (↑e) (comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f
rcases H with ⟨s, ⟨b⟩⟩
case pos.intro.intro.hMM'
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (Basis.map b e)) ↑e ⬝ ↑(toMatrix (Basis.map b e) b) ↑(LinearEquiv.symm e) = 1

case pos.intro.intro.hM'M
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (Basis.map b e) b) ↑(LinearEquiv.symm e) ⬝ ↑(toMatrix b (Basis.map b e)) ↑e = 1
case pos.intro.intro
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (comp (↑e) (comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f
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]
no goals
case pos.intro.intro.hMM'
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (Basis.map b e)) ↑e ⬝ ↑(toMatrix (Basis.map b e) b) ↑(LinearEquiv.symm e) = 1
rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
  toMatrix_id]
no goals
case pos.intro.intro.hM'M
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (Basis.map b e) b) ↑(LinearEquiv.symm e) ⬝ ↑(toMatrix b (Basis.map b e)) ↑e = 1
rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
  toMatrix_id]
case neg
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (comp (↑e) (comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f
case neg
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (comp (↑e) (comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f
have H' : ¬∃ t : Finset N, Nonempty (Basis t A N) := by
  contrapose! H
  rcases H with ⟨s, ⟨b⟩⟩
  exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩
no goals
case neg
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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 (comp (↑e) (comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f
simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg]
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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)
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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)
contrapose! H
case intro.intro
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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)
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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)
rcases H with ⟨s, ⟨b⟩⟩
no goals
case intro.intro
R : Type ?u.986725
inst✝¹¹ : CommRing R
M : Type u_3
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.987316
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.987858
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e✝ : Basis ι R M
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.988834
inst✝² : Fintype κ
N : Type u_1
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)
exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩