-- Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean
theorem charpoly_toMatrix {ι : Type w} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) :
    (toMatrix b b f).charpoly = f.charpoly

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : Matrix ι ι R := (toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type u_2 := ChooseBasisIndex R M
A' : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
⊢ ((toMatrix b b) f).charpoly = f.charpoly

Tactic:
let Q := b'.toMatrix b

Result:
R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : Matrix ι ι R := (toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type u_2 := ChooseBasisIndex R M
A' : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
⊢ ((toMatrix b b) f).charpoly = f.charpoly

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : Matrix ι ι R := (toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type u_2 := ChooseBasisIndex R M
A' : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
hPQ : C.mapMatrix (φ₁ P) * C.mapMatrix (φ₃ Q) = 1
⊢ ((scalar ι') X * C.mapMatrix (φ₁ P) * C.mapMatrix (φ₃ Q) -
        C.mapMatrix (φ₁ P) * C.mapMatrix A' * C.mapMatrix (φ₃ Q)).det =
    (C.mapMatrix (φ₁ P) * (scalar ι') X * C.mapMatrix (φ₃ Q) -
        C.mapMatrix (φ₁ P) * C.mapMatrix A' * C.mapMatrix (φ₃ Q)).det

Tactic:
rw [scalar_commute _ commute_X]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : Matrix ι ι R := (toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type u_2 := ChooseBasisIndex R M
A' : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
hPQ : C.mapMatrix (φ₁ P) * C.mapMatrix (φ₃ Q) = 1
⊢ (C.mapMatrix (φ₁ P) * (scalar ι') X * C.mapMatrix (φ₃ Q) -
        C.mapMatrix (φ₁ P) * C.mapMatrix A' * C.mapMatrix (φ₃ Q)).det =
    (C.mapMatrix (φ₁ P) * ((scalar ι') X - C.mapMatrix A') * C.mapMatrix (φ₃ Q)).det

Tactic:
rw [← Matrix.sub_mul, ← Matrix.mul_sub]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : Matrix ι ι R := (toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type u_2 := ChooseBasisIndex R M
A' : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
hPQ : C.mapMatrix (φ₁ P) * C.mapMatrix (φ₃ Q) = 1
⊢ (C.mapMatrix (φ₁ P)).det * ((scalar ι') X - C.mapMatrix A').det * (C.mapMatrix (φ₃ Q)).det =
    (C.mapMatrix (φ₁ P)).det * (C.mapMatrix (φ₃ Q)).det * ((scalar ι') X - C.mapMatrix A').det

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Nontrivial R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
A : Matrix ι ι R := (toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type u_2 := ChooseBasisIndex R M
A' : Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := (toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := b.indexEquiv b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := b.toMatrix ⇑b'
Q : Matrix (ChooseBasisIndex R M) ι R := b'.toMatrix ⇑b
hPQ : C.mapMatrix (φ₁ P) * C.mapMatrix (φ₃ Q) = 1
⊢ (C.mapMatrix (φ₁ P) * ((scalar ι') X - C.mapMatrix A') * C.mapMatrix (φ₃ Q)).det =
    (C.mapMatrix (φ₁ P)).det * ((scalar ι') X - C.mapMatrix A').det * (C.mapMatrix (φ₃ Q)).det

Tactic:
rw [det_mul, det_mul]

Result:
no goals