-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
theorem aeval_self_charpoly (M : Matrix n n R) : aeval M M.charpoly = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : M.charpoly • 1 = M.charmatrix.adjugate * M.charmatrix
⊢ (aeval M) M.charpoly = 0

Tactic:
apply_fun matPolyEquiv at h

Result:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : matPolyEquiv (M.charpoly • 1) = matPolyEquiv (M.charmatrix.adjugate * M.charmatrix)
⊢ (aeval M) M.charpoly = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : matPolyEquiv (M.charpoly • 1) = matPolyEquiv M.charmatrix.adjugate * (X - C M)
⊢ (aeval M) M.charpoly = 0

Tactic:
apply_fun fun p => p.eval M at h

Result:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (matPolyEquiv (M.charpoly • 1)) = eval M (matPolyEquiv M.charmatrix.adjugate * (X - C M))
⊢ (aeval M) M.charpoly = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (matPolyEquiv (M.charpoly • 1)) = 0
⊢ (aeval M) M.charpoly = 0

Tactic:
rw [matPolyEquiv_smul_one, eval_map] at h

Result:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval₂ (algebraMap R (Matrix n n R)) M M.charpoly = 0
⊢ (aeval M) M.charpoly = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : matPolyEquiv (M.charpoly • 1) = matPolyEquiv (M.charmatrix.adjugate * M.charmatrix)
⊢ (aeval M) M.charpoly = 0

Tactic:
simp only [_root_.map_mul, matPolyEquiv_charmatrix] at h

Result:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : matPolyEquiv (M.charpoly • 1) = matPolyEquiv M.charmatrix.adjugate * (X - C M)
⊢ (aeval M) M.charpoly = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (matPolyEquiv (M.charpoly • 1)) = eval M (matPolyEquiv M.charmatrix.adjugate * (X - C M))
⊢ (aeval M) M.charpoly = 0

Tactic:
rw [eval_mul_X_sub_C] at h

Result:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (matPolyEquiv (M.charpoly • 1)) = 0
⊢ (aeval M) M.charpoly = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval₂ (algebraMap R (Matrix n n R)) M M.charpoly = 0
⊢ (aeval M) M.charpoly = 0

Tactic:
exact h

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (aeval M) M.charpoly = 0

Tactic:
have h : M.charpoly • (1 : Matrix n n R[X]) = adjugate (charmatrix M) * charmatrix M :=
  (adjugate_mul _).symm

Result:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : M.charpoly • 1 = M.charmatrix.adjugate * M.charmatrix
⊢ (aeval M) M.charpoly = 0