awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∑ i : Fin n.succ,
      eval 0
        ((derivative : (a : R[X]) → R[X])
          (HPow.hPow (α := R[X]) (-1) (↑i : ℕ) *
              HAdd.hAdd (α := Matrix (Fin (n + 1)) (Fin (n + 1)) R[X]) 1
                (HSMul.hSMul (α := R[X]) (β := Matrix (Fin (n + 1)) (Fin (n + 1)) R[X]) X (M.map (⇑C : (a : R) → R[X])))
                0 i *
            ((1 +
                    HSMul.hSMul (α := R[X]) (β := Matrix (Fin (n + 1)) (Fin (n + 1)) R[X]) X
                      (M.map (⇑C : (a : R) → R[X]))).submatrix
                Fin.succ i.succAbove).det)) =
    M.trace
have succ : ∑ 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
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]
-- 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
⊢ ∑ 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 : (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
Tactic: rw [Finset.sum_eq_single 0]
-- 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
⊢ ∑ 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₁ : ∀ (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
Tactic: rw [Finset.sum_eq_single 0]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
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
h : 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
have succ : HPow.hPow (α := R) (-1) (↑i : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) 0) + M 0 i) *
    eval 0 (det (submatrix 1 Fin.succ i.succAbove)) =
  0
Tactic: simp only [one_apply_ne' hi, eval_zero, mul_zero, zero_add, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
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
h : Membership.mem (γ := Finset (Fin (n + 1).succ)) univ i
hi : i ≠ 0
⊢ HPow.hPow (α := R) (-1) (↑i : ℕ) * (eval 0 ((derivative : (a : R[X]) → R[X]) 0) + M 0 i) *
      eval 0 (det (submatrix 1 Fin.succ i.succAbove)) =
    0
have succ : ∀ (i_1 : Fin (n + 1)), Eq.{u + 1} (α := R[X]) (submatrix 1 Fin.succ i.succAbove i_1 0) 0
Tactic: rw [det_eq_zero_of_column_eq_zero 0, eval_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
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
h : Membership.mem (γ := Finset (Fin (n + 1).succ)) univ i
hi : i ≠ 0
j : Fin (n + 1)
⊢ Eq.{u + 1} (α := R[X]) (submatrix 1 Fin.succ i.succAbove j 0) 0
have succ : j.succ ≠ Fin.castSucc 0
Tactic: rw [submatrix_apply, Fin.succAbove_of_castSucc_lt, one_apply_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
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
h : Membership.mem (γ := Finset (Fin (n + 1).succ)) univ i
hi : i ≠ 0
j : Fin (n + 1)
succ : j.succ ≠ Fin.castSucc 0
⊢ Eq.{u + 1} (α := R[X]) (submatrix 1 Fin.succ i.succAbove j 0) 0
have succ₁ : Fin.castSucc 0 < i
Tactic: rw [submatrix_apply, Fin.succAbove_of_castSucc_lt, one_apply_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
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
h : Membership.mem (γ := Finset (Fin (n + 1).succ)) univ i
hi : i ≠ 0
j : Fin (n + 1)
⊢ Fin.castSucc 0 < i
have succ : 0 < i
Tactic: rw [Fin.castSucc_zero]
-- 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
i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.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) (Fin n) R[X]) X
                  ((M.submatrix Fin.succ i.succAbove).map (⇑C : (a : R) → R[X]))).det) =
    0
have 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
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
Cleared hypotheses: n, IH, M, i, h, hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
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
have zero : ∀ (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
Tactic: induction n with
  | zero => simp
  | succ n IH =>
    rw [det_succ_row_zero, map_sum, eval_finsetSum]
    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]
    rw [Finset.sum_eq_single 0]
    · 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]
    · intro i _ hi
      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
    · exact fun H ↦ (H <| Finset.mem_univ _).elim
Cleared hypotheses: n, M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Matrix (Fin n) (Fin n) R
zero :
  ∀ (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
⊢ 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
have succ : ∀ (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),
  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
Tactic: induction n with
  | zero => simp
  | succ n IH =>
    rw [det_succ_row_zero, map_sum, eval_finsetSum]
    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]
    rw [Finset.sum_eq_single 0]
    · 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]
    · intro i _ hi
      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
    · exact fun H ↦ (H <| Finset.mem_univ _).elim
Cleared hypotheses: n, M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ eval 0
      ((derivative : (a : R[X]) → R[X])
        (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det) =
    M.trace
have rw : eval 0
    ((derivative : (a : R[X]) → R[X])
      (det (n := Fin (Fintype.card n))
        ((reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
            (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
          (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])))))) =
  M.trace
Tactic: rw [← Matrix.det_reindexLinearEquiv_self R[X] (Fintype.equivFin n)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ eval 0
      ((derivative : (a : R[X]) → R[X])
        (det (n := Fin (Fintype.card n))
          ((reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
              (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
            (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])))))) =
    M.trace
have h : (reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
      (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
    (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))) =
  1 +
    HSMul.hSMul (α := R[X]) (β := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) X
      (map (α := R) ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
        (⇑C : (a : R) → R[X]))
Tactic: convert! derivative_det_one_add_X_smul_aux (e M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
h :
  (reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
        (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
      (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))) =
    1 +
      HSMul.hSMul (α := R[X]) (β := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) X
        (map (α := R) ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
          (⇑C : (a : R) → R[X]))
⊢ eval 0
      ((derivative : (a : R[X]) → R[X])
        (det (n := Fin (Fintype.card n))
          ((reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
              (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
            (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X])))))) =
    M.trace
have h₁ : M.trace =
  trace (n := Fin (Fintype.card n))
    ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
Tactic: convert! derivative_det_one_add_X_smul_aux (e M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ (reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
        (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
      (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))) =
    1 +
      HSMul.hSMul (α := R[X]) (β := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) X
        (map (α := R) ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
          (⇑C : (a : R) → R[X]))
have h : ∀ (i j : Fin (Fintype.card n)) (n_1 : ℕ),
  coeff
      ((reindexLinearEquiv R[X] R[X] (Fintype.equivFin n) (Fintype.equivFin n) :
          (a : Matrix n n R[X]) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X])
        (1 + HSMul.hSMul (α := R[X]) (β := Matrix.{v, v, u} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))) i j)
      n_1 =
    (HAdd.hAdd (α := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) 1
          (HSMul.hSMul (α := R[X]) (β := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R[X]) X
            (map (α := R) ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M)
              (⇑C : (a : R) → R[X])))
          i j).coeff
      n_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ Eq.{u + 1} (α := R) (∑ i : n, M.diag i)
    (∑ i : Fin (Fintype.card n),
      diag ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M) i)
have h : Eq.{u + 1} (α := R)
  (∑ i : Fin (Fintype.card n), M.diag ((Equiv.symm (Fintype.equivFin n) : (a : Fin (Fintype.card n)) → n) i))
  (∑ i : Fin (Fintype.card n),
    diag ((e : (a : Matrix n n R) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R) M) i)
Tactic: rw [← (Fintype.equivFin n).symm.sum_comp]