-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
lemma derivative_det_one_add_X_smul_aux {n} (M : Matrix (Fin n) (Fin n) R) :
    (derivative <| det (1 + (X : R[X]) • M.map C)).eval 0 = trace M

Proof state:
case succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ ∑ x : Fin n.succ,
      ((eval 0 (derivative ((-1) ^ ↑x)) * eval 0 (1 0 x) + (-1) ^ ↑x * (eval 0 (derivative (1 0 x)) + M 0 x)) *
          eval 0 (submatrix 1 Fin.succ x.succAbove).det +
        (-1) ^ ↑x * eval 0 (1 0 x) *
          eval 0 (derivative (submatrix 1 Fin.succ x.succAbove + X • (M.submatrix Fin.succ x.succAbove).map ⇑C).det)) =
    M.trace

Tactic:
rw [Finset.sum_eq_single 0]

Result:
case succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ (eval 0 (derivative ((-1) ^ ↑0)) * eval 0 (1 0 0) + (-1) ^ ↑0 * (eval 0 (derivative (1 0 0)) + M 0 0)) *
        eval 0 (submatrix 1 Fin.succ (Fin.succAbove 0)).det +
      (-1) ^ ↑0 * eval 0 (1 0 0) *
        eval 0
          (derivative
            (submatrix 1 Fin.succ (Fin.succAbove 0) + X • (M.submatrix Fin.succ (Fin.succAbove 0)).map ⇑C).det) =
    M.trace

case succ.h₀
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ ∀ b ∈ univ,
    b ≠ 0 →
      (eval 0 (derivative ((-1) ^ ↑b)) * eval 0 (1 0 b) + (-1) ^ ↑b * (eval 0 (derivative (1 0 b)) + M 0 b)) *
            eval 0 (submatrix 1 Fin.succ b.succAbove).det +
          (-1) ^ ↑b * eval 0 (1 0 b) *
            eval 0 (derivative (submatrix 1 Fin.succ b.succAbove + X • (M.submatrix Fin.succ b.succAbove).map ⇑C).det) =
        0

case succ.h₁
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ 0 ∉ univ →
    (eval 0 (derivative ((-1) ^ ↑0)) * eval 0 (1 0 0) + (-1) ^ ↑0 * (eval 0 (derivative (1 0 0)) + M 0 0)) *
          eval 0 (submatrix 1 Fin.succ (Fin.succAbove 0)).det +
        (-1) ^ ↑0 * eval 0 (1 0 0) *
          eval 0
            (derivative
              (submatrix 1 Fin.succ (Fin.succAbove 0) + X • (M.submatrix Fin.succ (Fin.succAbove 0)).map ⇑C).det) =
      0

Proof state:
case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ (-1) ^ ↑i * (eval 0 (derivative 0) + M 0 i) * eval 0 (submatrix 1 Fin.succ i.succAbove).det = 0

Tactic:
rw [det_eq_zero_of_column_eq_zero 0, eval_zero, mul_zero]

Result:
case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ ∀ (i_1 : Fin (n + 1)), submatrix 1 Fin.succ i.succAbove i_1 0 = 0

Proof state:
case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ ∀ (i_1 : Fin (n + 1)), submatrix 1 Fin.succ i.succAbove i_1 0 = 0

Tactic:
intro j

Result:
case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
j : Fin (n + 1)
⊢ submatrix 1 Fin.succ i.succAbove j 0 = 0

Proof state:
case zero
R : Type u
inst✝ : CommRing R
M : Matrix (Fin 0) (Fin 0) R
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace

Tactic:
simp

Result:
no goals

Proof state:
case succ.h₀
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
⊢ ∀ b ∈ univ,
    b ≠ 0 →
      (eval 0 (derivative ((-1) ^ ↑b)) * eval 0 (1 0 b) + (-1) ^ ↑b * (eval 0 (derivative (1 0 b)) + M 0 b)) *
            eval 0 (submatrix 1 Fin.succ b.succAbove).det +
          (-1) ^ ↑b * eval 0 (1 0 b) *
            eval 0 (derivative (submatrix 1 Fin.succ b.succAbove + X • (M.submatrix Fin.succ b.succAbove).map ⇑C).det) =
        0

Tactic:
intro i _ hi

Result:
case succ.h₀
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin n) (Fin n) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i : Fin n.succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ (eval 0 (derivative ((-1) ^ ↑i)) * eval 0 (1 0 i) + (-1) ^ ↑i * (eval 0 (derivative (1 0 i)) + M 0 i)) *
        eval 0 (submatrix 1 Fin.succ i.succAbove).det +
      (-1) ^ ↑i * eval 0 (1 0 i) *
        eval 0 (derivative (submatrix 1 Fin.succ i.succAbove + X • (M.submatrix Fin.succ i.succAbove).map ⇑C).det) =
    0

Proof state:
case succ.h₀.zero
R : Type u
inst✝ : CommRing R
IH : ∀ (M : Matrix (Fin 0) (Fin 0) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (0 + 1)) (Fin (0 + 1)) R
i : Fin (Nat.succ 0)
a✝ : i ∈ univ
hi : i ≠ 0
⊢ (eval 0 (derivative ((-1) ^ ↑i)) * eval 0 (1 0 i) + (-1) ^ ↑i * (eval 0 (derivative (1 0 i)) + M 0 i)) *
        eval 0 (submatrix 1 Fin.succ i.succAbove).det +
      (-1) ^ ↑i * eval 0 (1 0 i) *
        eval 0 (derivative (submatrix 1 Fin.succ i.succAbove + X • (M.submatrix Fin.succ i.succAbove).map ⇑C).det) =
    0

Tactic:
exact (hi (Subsingleton.elim i 0)).elim

Result:
no goals