-- 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
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace

Tactic:
rw [det_succ_row_zero, map_sum, eval_finset_sum]

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
⊢ ∑ i : Fin n.succ,
      eval 0
        (derivative ((-1) ^ ↑i * (1 + X • M.map ⇑C) 0 i * ((1 + X • M.map ⇑C).submatrix Fin.succ i.succAbove).det)) =
    M.trace

Proof state:
case succ.h₀.succ.h
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)
⊢ 0 < i

Tactic:
exact lt_of_le_of_ne (Fin.zero_le _) hi.symm

Result:
no goals

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
⊢ ∑ i : Fin n.succ,
      eval 0
        (derivative ((-1) ^ ↑i * (1 + X • M.map ⇑C) 0 i * ((1 + X • M.map ⇑C).submatrix Fin.succ i.succAbove).det)) =
    M.trace

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

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
⊢ ∑ 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

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
⊢ (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

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

Result:
no goals

Proof state:
case succ.h₀.succ.h
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)
⊢ Fin.castSucc 0 < i

Tactic:
rw [Fin.castSucc_zero]

Result:
case succ.h₀.succ.h
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)
⊢ 0 < i

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
j : Fin (n + 1)
⊢ j.succ ≠ Fin.castSucc 0

Tactic:
exact (bne_iff_ne (a := Fin.succ j) (b := Fin.castSucc 0)).mp rfl

Result:
no goals

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
j : Fin (n + 1)
⊢ submatrix 1 Fin.succ i.succAbove j 0 = 0

Tactic:
rw [submatrix_apply, Fin.succAbove_of_castSucc_lt, one_apply_ne]

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)
⊢ j.succ ≠ Fin.castSucc 0

case succ.h₀.succ.h
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)
⊢ Fin.castSucc 0 < i

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
⊢ 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:
exact fun H ↦ (H <| Finset.mem_univ _).elim

Result:
no goals

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
⊢ (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:
simp only [one_apply_ne' hi, eval_zero, mul_zero, zero_add, zero_mul, add_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
⊢ (-1) ^ ↑i * (eval 0 (derivative 0) + M 0 i) * eval 0 (submatrix 1 Fin.succ i.succAbove).det = 0