awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h_1 : Nontrivial R
h : ¬Fintype.card n = 0
mon :
  (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
          M.charpoly +
        M.charpoly).leadingCoeff =
    1
neg :
  (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
        M.charpoly).degree <
    degree M.charpoly
⊢ leadingCoeff M.charpoly = 1

Tactic:
rwa [leadingCoeff_add_of_degree_lt] at mon

Premises used: Polynomial.leadingCoeff_add_of_degree_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h_1 : Nontrivial R
h : ¬Fintype.card n = 0
mon :
  (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
          M.charpoly +
        M.charpoly).leadingCoeff =
    1
neg :
  (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
        M.charpoly).degree <
    (↑(Fintype.card n) : WithBot ℕ)
⊢ (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
        M.charpoly).degree <
    degree M.charpoly

Tactic:
rw [charpoly_degree_eq_dim]

Premises used: Matrix.charpoly_degree_eq_dim
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h_1 : Nontrivial R
h : ¬Fintype.card n = 0
mon :
  (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
          M.charpoly +
        M.charpoly).leadingCoeff =
    1
neg :
  (-HSub.hSub (α := R[X]) M.charpoly
          (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))).degree <
    (↑(Fintype.card n) : WithBot ℕ)
⊢ (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
        M.charpoly).degree <
    (↑(Fintype.card n) : WithBot ℕ)

Tactic:
rw [← neg_sub]

Premises used: neg_sub
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h_1 : Nontrivial R
h : ¬Fintype.card n = 0
mon :
  (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
          M.charpoly +
        M.charpoly).leadingCoeff =
    1
neg :
  (HSub.hSub (α := R[X]) M.charpoly
        (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))).degree <
    (↑(Fintype.card n) : WithBot ℕ)
⊢ (-HSub.hSub (α := R[X]) M.charpoly
          (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))).degree <
    (↑(Fintype.card n) : WithBot ℕ)

Tactic:
rw [degree_neg]

Premises used: Polynomial.degree_neg
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h_1 : Nontrivial R
h : ¬Fintype.card n = 0
mon :
  (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
          M.charpoly +
        M.charpoly).leadingCoeff =
    1
neg : LT.lt (α := WithBot ℕ) (↑(Fintype.card n - 1) : WithBot ℕ) (↑(Fintype.card n) : WithBot ℕ)
⊢ (HSub.hSub (α := R[X]) M.charpoly
        (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))).degree <
    (↑(Fintype.card n) : WithBot ℕ)

Tactic:
apply lt_trans (charpoly_sub_diagonal_degree_lt M)

Premises used: lt_trans, Matrix.charpoly_sub_diagonal_degree_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h_1 : Nontrivial R
h : ¬Fintype.card n = 0
mon :
  (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
          M.charpoly +
        M.charpoly).leadingCoeff =
    1
neg : Fintype.card n - 1 < Fintype.card n
⊢ LT.lt (α := WithBot ℕ) (↑(Fintype.card n - 1) : WithBot ℕ) (↑(Fintype.card n) : WithBot ℕ)

Tactic:
rw [Nat.cast_lt]

Premises used: Nat.cast_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h_1 : Nontrivial R
h : ¬Fintype.card n = 0
mon :
  (HSub.hSub (α := R[X]) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
          M.charpoly +
        M.charpoly).leadingCoeff =
    1
⊢ Fintype.card n - 1 < Fintype.card n

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Nonempty n
M : Matrix n n R
rw : Eq.{u + 1} (α := R) (∑ i : n, M.diag i) (∑ i : n, M i i)
⊢ M.trace = -coeff M.charpoly (Fintype.card n - 1)

Tactic:
rw [charpoly_coeff_eq_prod_coeff_of_le _ le_rfl, Fintype.card,
    prod_X_sub_C_coeff_card_pred univ (fun i : n => M i i) Fintype.card_pos, neg_neg, trace]

Premises used: le_rfl, Finset.univ, Matrix.trace, Fintype.card, neg_neg, Matrix.charpoly_coeff_eq_prod_coeff_of_le, Polynomial.prod_X_sub_C_coeff_card_pred, Fintype.card_pos
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Nonempty n
M : Matrix n n R
⊢ Eq.{u + 1} (α := R) (∑ i : n, M.diag i) (∑ i : n, M i i)

Tactic:
simp_rw [diag_apply]

Premises used: Matrix.diag_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
inl : IsEmpty n → M.trace = -nextCoeff M.charpoly
inr : Nonempty n → M.trace = -nextCoeff M.charpoly
⊢ M.trace = -nextCoeff M.charpoly

Tactic:
cases isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h : IsEmpty n
⊢ M.trace = -nextCoeff M.charpoly

Tactic:
simp [nextCoeff]

Premises used: Polynomial.nextCoeff
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h : Nonempty n
⊢ Nontrivial R

Tactic:
nontriviality
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h : Nonempty n
h_1 : Nontrivial R
⊢ M.trace = -nextCoeff M.charpoly

Tactic:
simp [trace_eq_neg_charpoly_coeff, nextCoeff]

Premises used: Matrix.trace_eq_neg_charpoly_coeff, Polynomial.nextCoeff
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
rw :
  M.det =
    (HSMul.hSMul (α := R) (-1)
        (eval ((scalar n : (a : R) → Matrix n n R) 0)
          (HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
            ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])))).det
⊢ M.det = HPow.hPow (α := R) (-1) (Fintype.card n) * coeff M.charpoly 0

Tactic:
rw [coeff_zero_eq_eval_zero, charpoly, eval_det, matPolyEquiv_charmatrix, ← det_smul]

Premises used: Polynomial.coeff_zero_eq_eval_zero, Matrix.det_smul, Matrix.matPolyEquiv_charmatrix, eval_det, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ M.det =
    (HSMul.hSMul (α := R) (-1)
        (eval ((scalar n : (a : R) → Matrix n n R) 0)
          (HSub.hSub (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X]) X
            ((C : (a : Matrix n n R) → (Matrix n n R)[X]) M : (Matrix n n R)[X])))).det

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
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:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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 :
  ∑ 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
⊢ 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:
rw [det_succ_row_zero, map_sum, eval_finsetSum]

Premises used: map_sum, Polynomial.eval_finsetSum, Matrix.det_succ_row_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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 :
  ∑ 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
⊢ ∑ 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

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]

Premises used: Polynomial.derivative_mul, eval_det_add_X_smul, Matrix.submatrix_smul, Polynomial.derivative_X, Polynomial.eval_C, Matrix.add_apply, Matrix.submatrix_add, Polynomial.eval_X, Polynomial.eval_pow, MulZeroClass.zero_mul, Polynomial.X_mul_C, Matrix.map_apply, map_add, Matrix.smul_apply, Polynomial.eval_mul, zero_add, MulZeroClass.mul_zero, Pi.add_apply, Polynomial.eval_add, Polynomial.eval_one, Polynomial.derivative_C, Polynomial.eval_neg, smul_eq_mul, mul_one, Matrix.submatrix_map, add_zero, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
⊢ (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:
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]

Premises used: Fin.succ_injective, Polynomial.eval_zero, zero_add, pow_zero, Matrix.submatrix_one, Matrix.trace_submatrix_succ, Polynomial.eval_one, Matrix.det_one, mul_one, Matrix.one_apply_eq, Fin.succAbove_zero, Fin.val_zero, Polynomial.derivative_one, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
succ :
  Membership.mem (γ := Finset (Fin n.succ)) univ i →
    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
⊢ Membership.mem (γ := Finset (Fin n.succ)) univ i →
    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

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
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)
h : 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:
(hi (Subsingleton.elim i 0)).elim

Premises used: False.elim, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
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)
h : 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:
exact (hi (Subsingleton.elim i 0)).elim

Premises used: False.elim, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
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
⊢ (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

Tactic:
simp only [one_apply_ne' hi, eval_zero, mul_zero, zero_add, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, Polynomial.eval_zero, zero_add, Matrix.one_apply_ne', MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
succ : ∀ (i_1 : Fin (n + 1)), Eq.{u + 1} (α := R[X]) (submatrix 1 Fin.succ i.succAbove i_1 0) 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

Tactic:
rw [det_eq_zero_of_column_eq_zero 0, eval_zero, mul_zero]

Premises used: Polynomial.eval_zero, MulZeroClass.mul_zero, Matrix.det_eq_zero_of_column_eq_zero, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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
succ₁ : Fin.castSucc 0 < i
⊢ Eq.{u + 1} (α := R[X]) (submatrix 1 Fin.succ i.succAbove j 0) 0

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

Premises used: Matrix.one_apply_ne, Fin.succAbove_of_castSucc_lt, Matrix.submatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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)
⊢ j.succ ≠ Fin.castSucc 0

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

Premises used: Iff.mp, bne_iff_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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)
⊢ j.succ ≠ Fin.castSucc 0

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

Premises used: Iff.mp, bne_iff_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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 : 0 < i
⊢ Fin.castSucc 0 < i

Tactic:
rw [Fin.castSucc_zero]

Premises used: Fin.castSucc_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
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)
⊢ 0 < i

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

Premises used: Fin.zero_le, Ne.symm, lt_of_le_of_ne