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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
rw :
  Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
    (HSMul.hSMul (α := R) (β := R[X])
      (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) c) : ℤ) : R)
      (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i))
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
    (HMul.hMul (α := R[X]) (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) c) : ℤ) : R[X])
      (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i))

Tactic:
rw [← C_eq_intCast, C_mul']

Premises used: Polynomial.C_mul', Polynomial.C_eq_intCast
-- 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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
apply :
  Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
    (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i)
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
    (HSMul.hSMul (α := R) (β := R[X])
      (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) c) : ℤ) : R)
      (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i))

Tactic:
apply Submodule.smul_mem (degreeLT R (Fintype.card n - 1)) ↑↑(Equiv.Perm.sign c)

Premises used: Polynomial.degreeLT, HSub.hSub, Fintype.card, OfNat.ofNat, Submodule.smul_mem
-- 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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
rw : degree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) < (↑(Fintype.card n - 1) : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
    (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i)

Tactic:
rw [mem_degreeLT]

Premises used: Polynomial.mem_degreeLT
-- 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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
apply :
  LT.lt (α := WithBot ℕ) (↑(natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i)) : WithBot ℕ)
    (↑(Fintype.card n - 1) : WithBot ℕ)
⊢ degree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) < (↑(Fintype.card n - 1) : WithBot ℕ)

Tactic:
apply lt_of_le_of_lt degree_le_natDegree _

Premises used: lt_of_le_of_lt, Polynomial.degree_le_natDegree
-- 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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
rw : natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) < Fintype.card n - 1
⊢ LT.lt (α := WithBot ℕ) (↑(natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i)) : WithBot ℕ)
    (↑(Fintype.card n - 1) : 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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
apply :
  natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) ≤
    card.{v} (α := n) {x : n | (c : (a : n) → n) x = x}
⊢ natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) < Fintype.card n - 1

Tactic:
apply lt_of_le_of_lt _ (Equiv.Perm.fixed_point_card_lt_of_ne_one (ne_of_mem_erase hc))

Premises used: lt_of_le_of_lt, Equiv.Perm.fixed_point_card_lt_of_ne_one, Finset.ne_of_mem_erase
-- 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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
apply : ∑ i : n, natDegree (M.charmatrix ((c : (a : n) → n) i) i) ≤ card.{v} (α := n) {x : n | (c : (a : n) → n) x = x}
⊢ natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) ≤
    card.{v} (α := n) {x : n | (c : (a : n) → n) x = x}

Tactic:
apply le_trans (Polynomial.natDegree_prod_le univ fun i : n => charmatrix M (c i) i) _

Premises used: Finset.univ, Polynomial.natDegree_prod_le, Matrix.charmatrix, DFunLike.coe, le_trans
-- 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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
rw :
  LE.le (α := ℕ) (∑ i : n, natDegree (M.charmatrix ((c : (a : n) → n) i) i)) (∑ x : n with (c : (a : n) → n) x = x, 1)
⊢ ∑ i : n, natDegree (M.charmatrix ((c : (a : n) → n) i) i) ≤ card.{v} (α := n) {x : n | (c : (a : n) → n) x = x}

Tactic:
rw [card_eq_sum_ones]

Premises used: Finset.card_eq_sum_ones
-- 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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
rw :
  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)
⊢ LE.le (α := ℕ) (∑ i : n, natDegree (M.charmatrix ((c : (a : n) → n) i) i)) (∑ x : n with (c : (a : n) → n) x = x, 1)

Tactic:
rw [sum_filter]

Premises used: Finset.sum_filter
-- 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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
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
⊢ 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)

Tactic:
apply sum_le_sum

Premises used: Finset.sum_le_sum
-- 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
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
i : n
h : 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 charmatrix_apply_natDegree_le

Premises used: Matrix.charmatrix_apply_natDegree_le
-- 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
k : ℕ
h : Fintype.card n - 1 ≤ k
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
⊢ 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

Tactic:
apply eq_of_sub_eq_zero

Premises used: eq_of_sub_eq_zero
-- 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
k : ℕ
h : Fintype.card n - 1 ≤ k
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
⊢ 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:
rw [← coeff_sub]

Premises used: Polynomial.coeff_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
k : ℕ
h : Fintype.card n - 1 ≤ k
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 ℕ)
⊢ (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:
apply Polynomial.coeff_eq_zero_of_degree_lt

Premises used: Polynomial.coeff_eq_zero_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
k : ℕ
h : Fintype.card n - 1 ≤ k
apply : LE.le (α := WithBot ℕ) (↑(Fintype.card n - 1) : WithBot ℕ) (↑k : 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 <
    (↑k : WithBot ℕ)

Tactic:
apply lt_of_lt_of_le (charpoly_sub_diagonal_degree_lt M) ?_

Premises used: Matrix.charpoly_sub_diagonal_degree_lt, lt_of_lt_of_le
-- 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
k : ℕ
h rw : Fintype.card n - 1 ≤ k
⊢ LE.le (α := WithBot ℕ) (↑(Fintype.card n - 1) : WithBot ℕ) (↑k : WithBot ℕ)

Tactic:
rw [Nat.cast_le]

Premises used: Nat.cast_le
-- 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
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ Fintype.card n - 1 ≤ k

Tactic:
apply h
-- 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 : Nontrivial R
M : Matrix n n R
pos : ∀ (h : Fintype.card n = 0), degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)
neg : ∀ (h : ¬Fintype.card n = 0), degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)
⊢ degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)

Tactic:
by_cases h : Fintype.card n = 0

Premises used: Fintype.card
-- 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 : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
pos : degree M.charpoly = (↑0 : WithBot ℕ)
⊢ degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)

Tactic:
rw [h]
-- 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 : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
pos : degree.{u} (R := R) 1 = (↑0 : WithBot ℕ)
pos₁ : Fintype.card n = 0
⊢ degree (det M.charmatrix) = (↑0 : WithBot ℕ)

Tactic:
rw [det_eq_one_of_card_eq_zero]

Premises used: Matrix.det_eq_one_of_card_eq_zero
-- 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 : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree.{u} (R := R) 1 = (↑0 : WithBot ℕ)

Tactic:
simp
-- 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 : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ Fintype.card n = 0

Tactic:
assumption
-- 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 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
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 ℕ)
⊢ degree M.charpoly = (↑(Fintype.card n) : WithBot ℕ)

Tactic:
rw [← sub_add_cancel M.charpoly (∏ i : n, (X - C (M i i)))]

Premises used: Polynomial.C, Finset.univ, HSub.hSub, Finset.prod, Polynomial.X, sub_add_cancel, DFunLike.coe, 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
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
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
⊢ 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:
rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']

Premises used: Polynomial.natDegree_prod', Polynomial.degree_eq_iff_natDegree_eq_of_pos, Nat.pos_of_ne_zero
-- 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 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
simp_rw : ∑ x : n, 1 = Fintype.card n
⊢ ∑ i : n, (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).natDegree = Fintype.card n

Tactic:
simp_rw [natDegree_X_sub_C]

Premises used: Polynomial.natDegree_X_sub_C
-- 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 : 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
rw₃ rw₄ : card.{v} (α := n) univ = card.{v} (α := n) univ
⊢ ∑ x : n, 1 = Fintype.card n

Tactic:
rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]

Premises used: Finset.card_univ, smul_eq_mul, mul_one, Finset.sum_const
-- 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 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h₁ : Ne.{u + 1} (α := R) (∏ x : n, 1) 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

Tactic:
simp_rw [(monic_X_sub_C _).leadingCoeff]

Premises used: Polynomial.monic_X_sub_C, Polynomial.Monic.leadingCoeff
-- 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 : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ Ne.{u + 1} (α := R) (∏ x : n, 1) 0

Tactic:
simp
-- 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 : 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 ℕ)

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
-- 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 : 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 ℕ)
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]))
⊢ (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 [degree_add_eq_right_of_degree_lt]

Premises used: Polynomial.degree_add_eq_right_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
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 ℕ)
⊢ 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:
h1
-- 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 : 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 ℕ)
⊢ 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:
exact h1
-- 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 : 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 :
  (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 <
    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 [h1]
-- 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 : 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 : 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
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 : 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
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 ℕ)
⊢ 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 : Nontrivial R
M : Matrix n n R
⊢ natDegree M.charpoly = Fintype.card n

Tactic:
natDegree_eq_of_degree_eq_some (charpoly_degree_eq_dim M)

Premises used: Matrix.charpoly_degree_eq_dim, Polynomial.natDegree_eq_of_degree_eq_some
-- 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
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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 : Nontrivial R
pos : ∀ (h : Fintype.card n = 0), Monic M.charpoly
neg : ∀ (h : ¬Fintype.card n = 0), Monic M.charpoly
⊢ Monic M.charpoly

Tactic:
by_cases h : Fintype.card n = 0

Premises used: Fintype.card
-- 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
pos : Monic.{u} (R := R) 1
⊢ Monic M.charpoly

Tactic:
rw [charpoly, det_eq_one_of_card_eq_zero h]

Premises used: Matrix.det_eq_one_of_card_eq_zero, 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
h_1 : Nontrivial R
h : Fintype.card n = 0
⊢ Monic.{u} (R := R) 1

Tactic:
apply monic_one

Premises used: Polynomial.monic_one
-- 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
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
⊢ Monic.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))

Tactic:
apply monic_prod_of_monic univ fun i : n => X - C (M i i)

Premises used: Polynomial.C, Finset.univ, HSub.hSub, Polynomial.monic_prod_of_monic, Polynomial.X, DFunLike.coe
-- 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
⊢ ∀ (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:
simp [monic_X_sub_C]

Premises used: Polynomial.monic_X_sub_C
-- 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
⊢ 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]
-- 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 : Monic.{u} (R := R) (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))
⊢ (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

Premises used: Polynomial.C, Finset.univ, HSub.hSub, Finset.prod, Polynomial.X, sub_add_cancel, DFunLike.coe, 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
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
⊢ (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 *

Premises used: Polynomial.Monic