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 : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ LE.le (α := ℕ) (∑ i : n, natDegree (M.charmatrix ((c : (a : n) → n) i) i))
    (∑ a : n, if (c : (a : n) → n) a = a then 1 else 0)
have h : ∀ (i : n),
  Membership.mem (γ := Finset n) univ i →
    natDegree (M.charmatrix ((c : (a : n) → n) i) i) ≤ if (c : (a : n) → n) i = i then 1 else 0
Tactic: apply sum_le_sum
-- 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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ coeff M.charpoly k = coeff (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) k
have h₁ : coeff M.charpoly k - coeff (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) k = 0
Tactic: apply eq_of_sub_eq_zero
-- 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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ coeff M.charpoly k - coeff (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) k = 0
have h₁ : (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]))).coeff
    k =
  0
Tactic: rw [← coeff_sub]
-- 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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ (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]))).coeff
      k =
    0
have h₁ : (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 <
  (↑k : WithBot ℕ)
Tactic: apply Polynomial.coeff_eq_zero_of_degree_lt
-- 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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ (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 <
    (↑k : WithBot ℕ)
have apply : LE.le (α := WithBot ℕ) (↑(Fintype.card n - 1) : WithBot ℕ) (↑k : WithBot ℕ)
Tactic: apply lt_of_lt_of_le (charpoly_sub_diagonal_degree_lt 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
inst_3 : Nontrivial R
M : Matrix n n R
⊢ degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)
have pos : ∀ (h : Fintype.card n = 0), degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)
Tactic: by_cases h : Fintype.card n = 0
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
pos : ∀ (h : Fintype.card n = 0), degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)
⊢ degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)
have neg : ∀ (h : ¬Fintype.card n = 0), degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)
Tactic: by_cases h : Fintype.card n = 0
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)
have pos : degree M.charpoly = (↑0 : WithBot ℕ)
Tactic: rw [h]
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree (det M.charmatrix) = (↑0 : WithBot ℕ)
have pos : degree.{u} (R := R) 1 = (↑0 : WithBot ℕ)
Tactic: rw [det_eq_one_of_card_eq_zero]
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)
have 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])) +
      ∏ 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 [← sub_add_cancel M.charpoly (∏ i : n, (X - C (M i i)))]
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ degree.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) =
    (↑(Fintype.card n) : WithBot ℕ)
have rw : ∑ i : n, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).natDegree = Fintype.card n
Tactic: rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
rw : ∑ i : n, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).natDegree = Fintype.card n
⊢ degree.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) =
    (↑(Fintype.card n) : WithBot ℕ)
have h₁ : Ne.{u + 1} (α := R) (∏ i : n, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).leadingCoeff)
  0
Tactic: rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ i : n, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).natDegree = Fintype.card n
have simp_rw : ∑ x : n, 1 = Fintype.card n
Tactic: simp_rw [natDegree_X_sub_C]
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ x : n, 1 = Fintype.card n
have rw : ∑ x : n, 1 = card.{v} (α := n) univ
Tactic: rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
rw : ∑ x : n, 1 = card.{v} (α := n) univ
⊢ ∑ x : n, 1 = Fintype.card n
have rw₁ : HSMul.hSMul (β := ℕ) (card.{v} (α := n) univ) 1 = card.{v} (α := n) univ
Tactic: rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
rw : ∑ x : n, 1 = card.{v} (α := n) univ
rw₁ : HSMul.hSMul (β := ℕ) (card.{v} (α := n) univ) 1 = card.{v} (α := n) univ
⊢ ∑ x : n, 1 = Fintype.card n
have rw₂ : card.{v} (α := n) univ * 1 = card.{v} (α := n) univ
Tactic: rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
rw : ∑ x : n, 1 = card.{v} (α := n) univ
rw₁ : HSMul.hSMul (β := ℕ) (card.{v} (α := n) univ) 1 = card.{v} (α := n) univ
rw₂ : card.{v} (α := n) univ * 1 = card.{v} (α := n) univ
⊢ ∑ x : n, 1 = Fintype.card n
have rw₃ : card.{v} (α := n) univ = card.{v} (α := n) univ
Tactic: rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ Ne.{u + 1} (α := R)
    (∏ i : n, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).leadingCoeff) 0
have h₁ : Ne.{u + 1} (α := R) (∏ x : n, 1) 0
Tactic: simp_rw [(monic_X_sub_C _).leadingCoeff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ (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])) +
        ∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).degree =
    (↑(Fintype.card n) : WithBot ℕ)
have h1 : degree.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) =
  (↑(Fintype.card n) : WithBot ℕ)
Tactic: have h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n) := by
    rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']
    · simp_rw [natDegree_X_sub_C]
      rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]
    simp_rw [(monic_X_sub_C _).leadingCoeff]
    simp
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 :
  degree.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) =
    (↑(Fintype.card n) : WithBot ℕ)
neg :
  degree.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) =
    (↑(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])) +
        ∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).degree =
    (↑(Fintype.card n) : WithBot ℕ)
have 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 <
  degree.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
Tactic: rw [degree_add_eq_right_of_degree_lt]
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 :
  degree.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) =
    (↑(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 <
    degree.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
have 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 ℕ)
Tactic: rw [h1]
-- 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 :
  degree.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) =
    (↑(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 ℕ)
have neg : LT.lt (α := WithBot ℕ) (↑(Fintype.card n - 1) : WithBot ℕ) (↑(Fintype.card n) : WithBot ℕ)
Tactic: apply lt_trans (charpoly_sub_diagonal_degree_lt 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
inst_3 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 :
  degree.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])) =
    (↑(Fintype.card n) : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ) (↑(Fintype.card n - 1) : WithBot ℕ) (↑(Fintype.card n) : WithBot ℕ)
have neg : Fintype.card n - 1 < Fintype.card n
Tactic: rw [Nat.cast_lt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ Monic M.charpoly
have a : Nontrivial R
Tactic: nontriviality R
-- 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
h : Nontrivial R
⊢ Monic M.charpoly
have pos : ∀ (h : Fintype.card n = 0), Monic M.charpoly
Tactic: by_cases h : Fintype.card n = 0
-- 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
h : Nontrivial R
pos : ∀ (h : Fintype.card n = 0), Monic M.charpoly
⊢ Monic M.charpoly
have neg : ∀ (h : ¬Fintype.card n = 0), Monic M.charpoly
Tactic: by_cases h : Fintype.card n = 0
-- 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
h_1 : Nontrivial R
h : Fintype.card n = 0
⊢ Monic M.charpoly
have pos : Monic.{u} (R := R) 1
Tactic: rw [charpoly, det_eq_one_of_card_eq_zero h]
-- 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
h_1 : Nontrivial R
h : ¬Fintype.card n = 0
⊢ Monic.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
have apply : ∀ (i : n),
  Membership.mem (γ := Finset n) univ i →
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).Monic
Tactic: apply monic_prod_of_monic univ fun i : n => X - C (M i i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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
⊢ Monic M.charpoly
have mon : Monic.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
Tactic: have mon : (∏ i : n, (X - C (M i i))).Monic := by
    apply monic_prod_of_monic univ fun i : n => X - C (M i i)
    simp [monic_X_sub_C]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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 : Monic.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
⊢ Monic M.charpoly
have 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).Monic
Tactic: rw [← sub_add_cancel (∏ i : n, (X - C (M i i))) M.charpoly] at mon
Cleared hypotheses: mon
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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).Monic
⊢ Monic M.charpoly
have 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
Tactic: rw [Monic] at *
Cleared hypotheses: mon
-- 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
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
⊢ leadingCoeff M.charpoly = 1
have 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
Tactic: rwa [leadingCoeff_add_of_degree_lt] at mon
-- 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
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
⊢ (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
have 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 ℕ)
Tactic: rw [charpoly_degree_eq_dim]
-- 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
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
⊢ (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 ℕ)
have 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 ℕ)
Tactic: rw [← neg_sub]
-- 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
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
⊢ (-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 ℕ)
have 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 ℕ)
Tactic: rw [degree_neg]
-- 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
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
⊢ (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 ℕ)
have neg : LT.lt (α := WithBot ℕ) (↑(Fintype.card n - 1) : WithBot ℕ) (↑(Fintype.card n) : WithBot ℕ)
Tactic: apply lt_trans (charpoly_sub_diagonal_degree_lt 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
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
⊢ LT.lt (α := WithBot ℕ) (↑(Fintype.card n - 1) : WithBot ℕ) (↑(Fintype.card n) : WithBot ℕ)
have neg : Fintype.card n - 1 < Fintype.card n
Tactic: rw [Nat.cast_lt]
-- 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
inst_3 : Nonempty n
M : Matrix n n R
⊢ M.trace = -coeff M.charpoly (Fintype.card n - 1)
have rw : Eq.{u + 1} (α := R) (∑ i : n, M.diag i) (∑ i : n, M i i)
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]
-- 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
⊢ M.trace = -nextCoeff M.charpoly
have inl : IsEmpty n → M.trace = -nextCoeff M.charpoly
Tactic: cases isEmpty_or_nonempty 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
inl : IsEmpty n → M.trace = -nextCoeff M.charpoly
⊢ M.trace = -nextCoeff M.charpoly
have inr : Nonempty n → M.trace = -nextCoeff M.charpoly
Tactic: cases isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (hypothesis)
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
⊢ M.trace = -nextCoeff M.charpoly
have a : Nontrivial R
Tactic: nontriviality
-- 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
⊢ M.det = HPow.hPow (α := R) (-1) (Fintype.card n) * coeff M.charpoly 0
have 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
Tactic: rw [coeff_zero_eq_eval_zero, charpoly, eval_det, matPolyEquiv_charmatrix, ← det_smul]
-- 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
⊢ 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
have 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
Tactic: rw [det_succ_row_zero, map_sum, eval_finsetSum]