Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: 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

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

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

Tactic:
]

Goal state after:
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