-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
theorem matPolyEquiv_charmatrix : matPolyEquiv (charmatrix M) = X - C M

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

Tactic:
rw [charmatrix_apply_ne _ _ _ h, coeff_X, coeff_neg, coeff_C, coeff_C]

Result:
case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (-if k = 0 then M i j else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i j

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ X.coeff k - (C (M i i)).coeff k = (X.coeff k - (C M).coeff k) i i

Tactic:
simp only [coeff_X, coeff_C]

Result:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i i

Proof state:
case a.a
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ (matPolyEquiv M.charmatrix).coeff k i j = (X - C M).coeff k i j

Tactic:
simp only [matPolyEquiv_coeff_apply, coeff_sub, Pi.sub_apply]

Result:
case a.a
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

Proof state:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ matPolyEquiv M.charmatrix = X - C M

Tactic:
ext k i j

Result:
case a.a
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ (matPolyEquiv M.charmatrix).coeff k i j = (X - C M).coeff k i j

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ (M.charmatrix i i).coeff k = (X.coeff k - (C M).coeff k) i i

Tactic:
rw [charmatrix_apply_eq, coeff_sub]

Result:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ X.coeff k - (C (M i i)).coeff k = (X.coeff k - (C M).coeff k) i i

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i i

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
case a.a
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

Tactic:
by_cases h : i = j

Result:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (-if k = 0 then M i j else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i j

Tactic:
split_ifs <;> simp [h]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

Tactic:
subst h

Result:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ (M.charmatrix i i).coeff k = (X.coeff k - (C M).coeff k) i i