-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin n) R
zero :
  ∀ (M : Matrix (Fin 0) (Fin 0) R),
    eval 0
        ((derivative : (a : R[X]) → R[X])
          (1 + HSMul.hSMul (α := R[X]) (β := Matrix (Fin 0) (Fin 0) R[X]) X (M.map (⇑C : (a : R) → R[X]))).det) =
      M.trace
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ (M : Matrix (Fin n) (Fin n) R),
        eval 0
            ((derivative : (a : R[X]) → R[X])
              (1 + HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X (M.map (⇑C : (a : R) → R[X]))).det) =
          M.trace)
    (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R),
    eval 0
        ((derivative : (a : R[X]) → R[X])
          (1 +
              HSMul.hSMul (α := R[X]) (β := Matrix (Fin (n + 1)) (Fin (n + 1)) R[X]) X
                (M.map (⇑C : (a : R) → R[X]))).det) =
      M.trace
⊢ eval 0
      ((derivative : (a : R[X]) → R[X])
        (1 + HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X (M.map (⇑C : (a : R) → R[X]))).det) =
    M.trace

Tactic:
induction n with
  | zero => simp
  | succ n IH =>
    rw [det_succ_row_zero, map_sum, eval_finsetSum]
    simp only [add_apply, smul_apply, map_apply, smul_eq_mul, X_mul_C, submatrix_add,
      submatrix_smul, Pi.add_apply, Pi.smul_apply, submatrix_map, derivative_mul, map_add,
      derivative_C, zero_mul, derivative_X, mul_one, zero_add, eval_add, eval_mul, eval_C, eval_X,
      mul_zero, add_zero, eval_det_add_X_smul, eval_pow, eval_neg, eval_one]
    rw [Finset.sum_eq_single 0]
    · simp only [Fin.val_zero, pow_zero, derivative_one, eval_zero, one_apply_eq, eval_one,
        mul_one, zero_add, one_mul, Fin.succAbove_zero, submatrix_one _ (Fin.succ_injective _),
        det_one, IH, trace_submatrix_succ]
    · intro i _ hi
      cases n with
      | zero => exact (hi (Subsingleton.elim i 0)).elim
      | succ n =>
        simp only [one_apply_ne' hi, eval_zero, mul_zero, zero_add, zero_mul, add_zero]
        rw [det_eq_zero_of_column_eq_zero 0, eval_zero, mul_zero]
        intro j
        rw [submatrix_apply, Fin.succAbove_of_castSucc_lt, one_apply_ne]
        · exact (bne_iff_ne (a := Fin.succ j) (b := Fin.castSucc 0)).mp rfl
        · rw [Fin.castSucc_zero]; exact lt_of_le_of_ne (Fin.zero_le _) hi.symm
    · exact fun H ↦ (H <| Finset.mem_univ _).elim

Premises used: Polynomial.derivative_mul, eval_det_add_X_smul, Matrix.submatrix_smul, Polynomial.derivative_X, Polynomial.eval_C, Matrix.add_apply, Matrix.submatrix_add, Polynomial.eval_X, Polynomial.eval_pow, MulZeroClass.zero_mul, Polynomial.X_mul_C, Matrix.one_apply_ne, Matrix.map_apply, Fin.succ_injective, map_add, Matrix.smul_apply, Polynomial.eval_mul, map_sum, Polynomial.eval_zero, zero_add, Polynomial.eval_finsetSum, Finset.sum_eq_single, pow_zero, MulZeroClass.mul_zero, Pi.add_apply, Matrix.submatrix_one, Fin.castSucc_zero, Matrix.trace_submatrix_succ, Polynomial.eval_add, Polynomial.eval_one, Fin.succAbove_of_castSucc_lt, Matrix.det_one, Polynomial.derivative_C, Polynomial.eval_neg, Matrix.submatrix_apply, Matrix.det_eq_zero_of_column_eq_zero, smul_eq_mul, mul_one, Matrix.one_apply_eq, Matrix.submatrix_map, Fin.succAbove_zero, add_zero, OfNat.ofNat, Matrix.det_succ_row_zero, Matrix.zero, Fin.val_zero, Polynomial.derivative_one, one_mul, Pi.smul_apply