-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
succ :
  (HMul.hMul (α := R) (eval 0 ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (-1) (↑0 : ℕ))))
            (eval 0 (1 0 0)) +
          HPow.hPow (α := R) (-1) (↑0 : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) (1 0 0)) + M 0 0)) *
        eval 0 (det (n := Fin n) (submatrix 1 Fin.succ (Fin.succAbove 0))) +
      HPow.hPow (α := R) (-1) (↑0 : ℕ) * eval 0 (1 0 0) *
        eval 0
          ((derivative : (a : R[X]) → R[X])
            (submatrix 1 Fin.succ (Fin.succAbove 0) +
                HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X
                  ((M.submatrix Fin.succ (Fin.succAbove 0)).map (⇑C : (a : R) → R[X]))).det) =
    M.trace
succ₁ :
  ∀ (b : Fin n.succ),
    Membership.mem (γ := Finset (Fin n.succ)) univ b →
      b ≠ 0 →
        (HMul.hMul (α := R) (eval 0 ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (-1) (↑b : ℕ))))
                  (eval 0 (1 0 b)) +
                HPow.hPow (α := R) (-1) (↑b : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) (1 0 b)) + M 0 b)) *
              eval 0 (det (submatrix 1 Fin.succ b.succAbove)) +
            HPow.hPow (α := R) (-1) (↑b : ℕ) * eval 0 (1 0 b) *
              eval 0
                ((derivative : (a : R[X]) → R[X])
                  (submatrix 1 Fin.succ b.succAbove +
                      HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X
                        ((M.submatrix Fin.succ b.succAbove).map (⇑C : (a : R) → R[X]))).det) =
          0
⊢ ∑ x : Fin n.succ,
      ((HMul.hMul (α := R) (eval 0 ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (-1) (↑x : ℕ))))
              (eval 0 (1 0 x)) +
            HPow.hPow (α := R) (-1) (↑x : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) (1 0 x)) + M 0 x)) *
          eval 0 (det (submatrix 1 Fin.succ x.succAbove)) +
        HPow.hPow (α := R) (-1) (↑x : ℕ) * eval 0 (1 0 x) *
          eval 0
            ((derivative : (a : R[X]) → R[X])
              (submatrix 1 Fin.succ x.succAbove +
                  HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X
                    ((M.submatrix Fin.succ x.succAbove).map (⇑C : (a : R) → R[X]))).det)) =
    M.trace
have succ₂ : 0 ∉ univ →
  (HMul.hMul (α := R) (eval 0 ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (-1) (↑0 : ℕ))))
            (eval 0 (1 0 0)) +
          HPow.hPow (α := R) (-1) (↑0 : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) (1 0 0)) + M 0 0)) *
        eval 0 (det (n := Fin n) (submatrix 1 Fin.succ (Fin.succAbove 0))) +
      HPow.hPow (α := R) (-1) (↑0 : ℕ) * eval 0 (1 0 0) *
        eval 0
          ((derivative : (a : R[X]) → R[X])
            (submatrix 1 Fin.succ (Fin.succAbove 0) +
                HSMul.hSMul (α := R[X]) (β := Matrix (Fin n) (Fin n) R[X]) X
                  ((M.submatrix Fin.succ (Fin.succAbove 0)).map (⇑C : (a : R) → R[X]))).det) =
    0
Tactic: rw [Finset.sum_eq_single 0]