-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem matPolyEquiv_eq_X_pow_sub_C {K : Type*} (k : ℕ) [Field K] (M : Matrix n n K) :
    matPolyEquiv ((expand K k : K[X] →+* K[X]).mapMatrix (charmatrix (M ^ k))) =
      X ^ k - C (M ^ k)

Proof state:
case a.a
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = (if m = k then 1 else 0) i j - (if m = 0 then M ^ k else 0) i j

Tactic:
by_cases hij : i = j

Result:
case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = (if m = k then 1 else 0) i j - (if m = 0 then M ^ k else 0) i j

case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = (if m = k then 1 else 0) i j - (if m = 0 then M ^ k else 0) i j

Proof state:
case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ ((if m = k then 1 else 0) - if m = 0 then (M ^ k) j j else 0) =
    (if m = k then 1 else 0) j j - (if m = 0 then M ^ k else 0) j j

Tactic:
split_ifs with mp m0 <;> simp only [Matrix.one_apply_eq, Matrix.zero_apply]

Result:
no goals

Proof state:
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
⊢ matPolyEquiv ((↑(expand K k)).mapMatrix (M ^ k).charmatrix) = X ^ k - C (M ^ k)

Tactic:
ext m i j

Result:
case a.a
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
⊢ (matPolyEquiv ((↑(expand K k)).mapMatrix (M ^ k).charmatrix)).coeff m i j = (X ^ k - C (M ^ k)).coeff m i j

Proof state:
case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
⊢ (-if m = 0 then (M ^ k) i j else 0) = (if m = k then 1 else 0) i j - (if m = 0 then M ^ k else 0) i j

Tactic:
split_ifs with m0 mp <;>
  simp only [hij, zero_sub, Matrix.zero_apply, sub_zero, neg_zero, Matrix.one_apply_ne, Ne,
    not_false_iff]

Result:
no goals

Proof state:
case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = (if m = k then 1 else 0) i j - (if m = 0 then M ^ k else 0) i j

Tactic:
rw [charmatrix_apply_ne _ _ _ hij, map_neg, expand_C, coeff_neg, coeff_C]

Result:
case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : ¬i = j
⊢ (-if m = 0 then (M ^ k) i j else 0) = (if m = k then 1 else 0) i j - (if m = 0 then M ^ k else 0) i j

Proof state:
case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = (if m = k then 1 else 0) i j - (if m = 0 then M ^ k else 0) i j

Tactic:
rw [hij, charmatrix_apply_eq, map_sub, expand_C, expand_X, coeff_sub, coeff_X_pow, coeff_C]

Result:
case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ ((if m = k then 1 else 0) - if m = 0 then (M ^ k) j j else 0) =
    (if m = k then 1 else 0) j j - (if m = 0 then M ^ k else 0) j j

Proof state:
case a.a
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
⊢ (matPolyEquiv ((↑(expand K k)).mapMatrix (M ^ k).charmatrix)).coeff m i j = (X ^ k - C (M ^ k)).coeff m i j

Tactic:
rw [coeff_sub, coeff_C, matPolyEquiv_coeff_apply, RingHom.mapMatrix_apply, Matrix.map_apply,
  AlgHom.coe_toRingHom, DMatrix.sub_apply, coeff_X_pow]

Result:
case a.a
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : Field K
M : Matrix n n K
m : ℕ
i j : n
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = (if m = k then 1 else 0) i j - (if m = 0 then M ^ k else 0) i j