-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
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
i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i
hi : i ≠ 0
succ :
  ∀
    (IH :
      ∀ (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)
    (M : Matrix (Fin (HAdd.hAdd (α := ℕ) 0 1)) (Fin (HAdd.hAdd (α := ℕ) 0 1)) R) (i : Fin (Nat.succ 0)),
    Membership.mem (γ := Finset (Fin (Nat.succ 0))) univ i →
      ∀ (hi : i ≠ 0),
        (HMul.hMul (α := R) (eval 0 ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (-1) (↑i : ℕ))))
                  (eval 0 (1 0 i)) +
                HPow.hPow (α := R) (-1) (↑i : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) (1 0 i)) + M 0 i)) *
              eval 0 (det (submatrix 1 Fin.succ i.succAbove)) +
            HPow.hPow (α := R) (-1) (↑i : ℕ) * eval 0 (1 0 i) *
              eval 0
                ((derivative : (a : R[X]) → R[X])
                  (submatrix 1 Fin.succ i.succAbove +
                      HSMul.hSMul (α := R[X]) (β := Matrix (Fin 0) (Fin 0) R[X]) X
                        ((M.submatrix Fin.succ i.succAbove).map (⇑C : (a : R) → R[X]))).det) =
          0
succ₁ :
  ∀ (n : ℕ)
    (IH :
      ∀ (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)
    (M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R) (i : Fin (n + 1).succ),
    Membership.mem (γ := Finset (Fin (n + 1).succ)) univ i →
      ∀ (hi : i ≠ 0),
        (HMul.hMul (α := R) (eval 0 ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (-1) (↑i : ℕ))))
                  (eval 0 (1 0 i)) +
                HPow.hPow (α := R) (-1) (↑i : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) (1 0 i)) + M 0 i)) *
              eval 0 (det (submatrix 1 Fin.succ i.succAbove)) +
            HPow.hPow (α := R) (-1) (↑i : ℕ) * eval 0 (1 0 i) *
              eval 0
                ((derivative : (a : R[X]) → R[X])
                  (submatrix 1 Fin.succ i.succAbove +
                      HSMul.hSMul (α := R[X]) (β := Matrix (Fin (n + 1)) (Fin (n + 1)) R[X]) X
                        ((M.submatrix Fin.succ i.succAbove).map (⇑C : (a : R) → R[X]))).det) =
          0
⊢ (HMul.hMul (α := R) (eval 0 ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (-1) (↑i : ℕ))))
            (eval 0 (1 0 i)) +
          HPow.hPow (α := R) (-1) (↑i : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) (1 0 i)) + M 0 i)) *
        eval 0 (det (submatrix 1 Fin.succ i.succAbove)) +
      HPow.hPow (α := R) (-1) (↑i : ℕ) * eval 0 (1 0 i) *
        eval 0
          ((derivative : (a : R[X]) → R[X])
            (submatrix 1 Fin.succ i.succAbove +
                HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X
                  ((M.submatrix Fin.succ i.succAbove).map (⇑C : (a : R) → R[X]))).det) =
    0

Tactic:
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

Premises used: MulZeroClass.zero_mul, Matrix.one_apply_ne, Fin.zero_le, Ne.symm, Polynomial.eval_zero, zero_add, Matrix.one_apply_ne', MulZeroClass.mul_zero, Fin.castSucc_zero, Fin.succAbove_of_castSucc_lt, Matrix.submatrix_apply, Matrix.det_eq_zero_of_column_eq_zero, add_zero, OfNat.ofNat, Matrix.zero, lt_of_le_of_ne