awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X])).leadingCoeff =
    a
rw₁ :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X]) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)).leadingCoeff =
    a
rw₂ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)).leadingCoeff = a
rw₃ rw₄ : a = a
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).leadingCoeff =
    a

Tactic:
rw [add_assoc, add_comm, leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    leadingCoeff_C_mul_X_pow]

Premises used: add_assoc, add_comm, Polynomial.leadingCoeff_C_mul_X_pow, Polynomial.leadingCoeff_add_of_degree_lt, Polynomial.degree_linear_lt_degree_C_mul_X_sq
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c d : R
inst : Semiring R
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).degree ≤
    3

Tactic:
simpa only [add_assoc] using
    degree_add_le_of_degree_le (degree_C_mul_X_pow_le 3 a)
      (le_trans degree_quadratic_le <| WithBot.coe_le_coe.mpr <| Nat.le_succ 2)

Premises used: Iff.mpr, add_assoc, Polynomial.degree_quadratic_le, Nat.le_succ, Polynomial.degree_C_mul_X_pow_le, WithBot.coe_le_coe, Polynomial.degree_add_le_of_degree_le, OfNat.ofNat, le_trans
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c d : R
inst : Semiring R
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).degree <
    4

Tactic:
degree_cubic_le.trans_lt <| WithBot.coe_lt_coe.mpr <| lt_add_one 3

Premises used: Iff.mpr, lt_add_one, WithBot.coe_lt_coe, Polynomial.degree_cubic_le, OfNat.ofNat, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).degree <
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3)).degree

Tactic:
simpa only [degree_C_mul_X_pow 3 ha] using degree_quadratic_lt

Premises used: Polynomial.degree_quadratic_lt, OfNat.ofNat, Polynomial.degree_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
rw : Eq (α := WithBot ℕ) (↑3 : WithBot ℕ) 3
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).degree =
    3

Tactic:
rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2),
    degree_add_eq_left_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    degree_C_mul_X_pow 3 ha]

Premises used: Polynomial.C, HMul.hMul, add_assoc, Polynomial.degree_add_eq_left_of_degree_lt, HPow.hPow, Polynomial.degree_quadratic_lt_degree_C_mul_X_cb, OfNat.ofNat, Polynomial.X, DFunLike.coe, Polynomial.degree_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
⊢ Eq (α := WithBot ℕ) (↑3 : WithBot ℕ) 3

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c d : R
inst : Semiring R
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).natDegree ≤
    3

Tactic:
natDegree_le_of_degree_le degree_cubic_le

Premises used: Polynomial.natDegree_le_of_degree_le, Polynomial.degree_cubic_le
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).natDegree =
    3

Tactic:
natDegree_eq_of_degree_eq_some <| degree_cubic ha

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_cubic
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c d : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
            ((C : (a : R) → R[X]) d : R[X]))).leadingCoeff =
    a
rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a
rw₃ :
  (HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
          ((C : (a : R) → R[X]) d : R[X]) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3)).leadingCoeff =
    a
rw₄ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3)).leadingCoeff = a
rw₅ rw₆ : a = a
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
        ((C : (a : R) → R[X]) d : R[X])).leadingCoeff =
    a

Tactic:
rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
    leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
    leadingCoeff_C_mul_X_pow]

Premises used: Polynomial.C, HMul.hMul, add_assoc, add_comm, Polynomial.leadingCoeff_C_mul_X_pow, HPow.hPow, Polynomial.leadingCoeff_add_of_degree_lt, Polynomial.degree_quadratic_lt_degree_C_mul_X_cb, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
inl : AddMonoidAlgebra.supDegree.{u, 0, 0} (R := R) id (toFinsupp 0) = natDegree.{u} (R := R) 0
inr : ∀ (h : p ≠ 0), AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

Tactic:
obtain rfl | h := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
⊢ AddMonoidAlgebra.supDegree.{u, 0, 0} (R := R) id (toFinsupp 0) = natDegree.{u} (R := R) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
inr : (↑(AddMonoidAlgebra.supDegree id p.toFinsupp) : WithBot ℕ) = (↑p.natDegree : WithBot ℕ)
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

Tactic:
apply WithBot.coe_injective

Premises used: WithBot.coe_injective
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
inr : p.toFinsupp.support.Nonempty
⊢ (↑(AddMonoidAlgebra.supDegree id p.toFinsupp) : WithBot ℕ) = (↑p.natDegree : WithBot ℕ)

Tactic:
rw [← AddMonoidAlgebra.supDegree_withBot_some_comp, Function.comp_id, supDegree_eq_degree,
    degree_eq_natDegree h, Nat.cast_withBot]

Premises used: Function.comp_id, Polynomial.degree_eq_natDegree, Polynomial.supDegree_eq_degree, Nat.cast_withBot, AddMonoidAlgebra.supDegree_withBot_some_comp
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
inr : p.support.Nonempty
inr₁ : p.support ≠ ∅
inr₂ : ¬p.support = ∅
inr₃ inr₄ inr₅ inr₆ : ¬p = 0
⊢ p.toFinsupp.support.Nonempty

Tactic:
rwa [support_toFinsupp, nonempty_iff_ne_empty, Ne, support_eq_empty]

Premises used: Ne, Finset.nonempty_iff_ne_empty, Polynomial.support_eq_empty, Polynomial.support_toFinsupp
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : ℕ
⊢ a ∈ p.support → a ≤ p.natDegree

Tactic:
le_natDegree_of_ne_zero ∘ mem_support_iff.mp

Premises used: Function.comp, Polynomial.mem_support_iff, Iff.mp, Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
m : ℕ
inst : Semiring R
p : R[X]
h : p.natDegree < m
⊢ p.support ⊆ range m

Tactic:
fun _n hn =>
  mem_range.2 <| (le_natDegree_of_mem_supp _ hn).trans_lt h

Premises used: Iff.mpr, Polynomial.le_natDegree_of_mem_supp, Finset.mem_range, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.support ⊆ range (p.natDegree + 1)

Tactic:
supp_subset_range (Nat.lt_succ_self _)

Premises used: Polynomial.supp_subset_range, Nat.lt_succ_self
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p = ∑ i ∈ p.support, (monomial i : (a : R) → R[X]) (p.coeff i)

Tactic:
(sum_monomial_eq p).symm

Premises used: Polynomial.sum, Polynomial.sum_monomial_eq, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ Eq.{u + 1} (α := R[X]) (∑ i ∈ p.support, (monomial i : (a : R) → R[X]) (p.coeff i))
    (∑ i ∈ p.support, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))

Tactic:
simp only [C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
hn : p.natDegree < n
⊢ p.support ⊆ range n

Tactic:
have := supp_subset_range hn
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
hn : p.natDegree < n
this : p.support ⊆ range n
simp :
  Eq.{v + 1} (α := S) (∑ x ∈ p.toFinsupp.support, f x ((p.toFinsupp : (a : ℕ) → R) x))
    (∑ x ∈ range n, f x ((p.toFinsupp : (a : ℕ) → R) x))
⊢ p.sum f = ∑ a ∈ range n, f a (p.coeff a)

Tactic:
simp only [Polynomial.sum, support, coeff] at this ⊢

Premises used: Polynomial.sum, Polynomial.coeff, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
hn : p.natDegree < n
this : p.toFinsupp.support ⊆ range n
⊢ Eq.{v + 1} (α := S) (∑ x ∈ p.toFinsupp.support, f x ((p.toFinsupp : (a : ℕ) → R) x))
    (∑ x ∈ range n, f x ((p.toFinsupp : (a : ℕ) → R) x))

Tactic:
Finsupp.sum_of_support_subset _ this _ fun n _hn => h n

Premises used: Finsupp.sum, Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
n : ℕ
hn : p.natDegree < n
this : p.toFinsupp.support ⊆ range n
⊢ Eq.{v + 1} (α := S) (∑ x ∈ p.toFinsupp.support, f x ((p.toFinsupp : (a : ℕ) → R) x))
    (∑ x ∈ range n, f x ((p.toFinsupp : (a : ℕ) → R) x))

Tactic:
exact Finsupp.sum_of_support_subset _ this _ fun n _hn => h n

Premises used: Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
p : R[X]
f : ℕ → R → S
h : ∀ (n : ℕ), f n 0 = 0
⊢ p.sum f = ∑ a ∈ range (p.natDegree + 1), f a (p.coeff a)

Tactic:
sum_over_range' p h (p.natDegree + 1) (lt_add_one _)

Premises used: lt_add_one, HAdd.hAdd, Polynomial.sum_over_range', Polynomial.natDegree, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
pos : ∀ (hp : p = 0), ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f
neg : ∀ (hp : ¬p = 0), ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f
⊢ ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
hp : p = 0
pos : ∀ (x : Fin n), Membership.mem (γ := Finset (Fin n)) univ x → f (↑x : ℕ) (coeff 0 (↑x : ℕ)) = 0
⊢ ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f

Tactic:
rw [hp, sum_zero_index, Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero, Polynomial.sum_zero_index
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
hp : p = 0
i : Fin n
pos : Membership.mem (γ := Finset (Fin n)) univ i → f (↑i : ℕ) (coeff 0 (↑i : ℕ)) = 0
⊢ Membership.mem (γ := Finset (Fin n)) univ i → f (↑i : ℕ) (coeff 0 (↑i : ℕ)) = 0

Tactic:
_
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
hp : p = 0
i : Fin n
h : Membership.mem (γ := Finset (Fin n)) univ i
⊢ f (↑i : ℕ) (coeff 0 (↑i : ℕ)) = 0

Tactic:
hf i

Premises used: Fin.val, Polynomial.coeff
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
hp : p = 0
i : Fin n
h : Membership.mem (γ := Finset (Fin n)) univ i
⊢ f (↑i : ℕ) (coeff 0 (↑i : ℕ)) = 0

Tactic:
exact hf i

Premises used: Fin.val
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < (↑n : WithBot ℕ)
hp : ¬p = 0
neg : Eq.{v + 1} (α := S) (∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ))) (∑ a ∈ range n, f a (p.coeff a))
neg₁ neg₂ : Eq.{v + 1} (α := S) (∑ i ∈ range n, f i (p.coeff i)) (∑ a ∈ range n, f a (p.coeff a))
⊢ ∑ i : Fin n, f (↑i : ℕ) (p.coeff (↑i : ℕ)) = p.sum f

Tactic:
rw [sum_over_range' _ hf n ((natDegree_lt_iff_degree_lt hp).mpr hn),
    Fin.sum_univ_eq_sum_range fun i => f i (p.coeff i)]

Premises used: Iff.mpr, Fin.sum_univ_eq_sum_range, Polynomial.natDegree_lt_iff_degree_lt, Polynomial.coeff, Polynomial.sum_over_range'
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ p = ∑ i ∈ range n, (monomial i : (a : R) → R[X]) (p.coeff i)

Tactic:
p.sum_monomial_eq.symm.trans <| p.sum_over_range' monomial_zero_right _ hn

Premises used: Polynomial.sum_monomial_eq, Polynomial.monomial_zero_right, Polynomial.sum_over_range', Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p = ∑ i ∈ range (p.natDegree + 1), (monomial i : (a : R) → R[X]) (p.coeff i)

Tactic:
p.as_sum_range' _ (lt_add_one _)

Premises used: lt_add_one, Polynomial.as_sum_range'
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ Eq.{u + 1} (α := R[X]) (∑ i ∈ range n, (monomial i : (a : R) → R[X]) (p.coeff i))
    (∑ i ∈ range n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))

Tactic:
simp only [C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p =
    ∑ i ∈ range (p.natDegree + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)

Tactic:
p.as_sum_range_C_mul_X_pow' (lt_add_one _)

Premises used: Polynomial.as_sum_range_C_mul_X_pow', lt_add_one
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
n a : ℕ
c : R
h : a ∈ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X n)).support
⊢ a = n

Tactic:
mem_singleton.1 <| support_C_mul_X_pow' n c h

Premises used: Finset.mem_singleton, Polynomial.support_C_mul_X_pow', Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
c : R
n : ℕ
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X n)).support ≤ card (α := ℕ) {n}

Tactic:
apply card_le_card (support_C_mul_X_pow' n c)

Premises used: Finset.card_le_card, Polynomial.support_C_mul_X_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : #p.support ≤ #(range (p.natDegree + 1))
⊢ #p.support ≤ p.natDegree + 1

Tactic:
rw [← Finset.card_range (p.natDegree + 1)]

Premises used: Finset.card_range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ #p.support ≤ #(range (p.natDegree + 1))

Tactic:
Finset.card_le_card supp_subset_range_natDegree_succ

Premises used: Finset.card_le_card, Polynomial.supp_subset_range_natDegree_succ
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ #p.support ≤ #(range (p.natDegree + 1))

Tactic:
exact Finset.card_le_card supp_subset_range_natDegree_succ

Premises used: Finset.card_le_card, Polynomial.supp_subset_range_natDegree_succ
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : ℕ
⊢ a ∈ p.support → (↑a : WithBot ℕ) ≤ p.degree

Tactic:
le_degree_of_ne_zero ∘ mem_support_iff.mp

Premises used: Function.comp, Polynomial.mem_support_iff, Iff.mp, Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.support.Nonempty ↔ ¬p = 0
rw₁ : p.support ≠ ∅ ↔ ¬p = 0
rw₂ : ¬p.support = ∅ ↔ ¬p = 0
rw₃ rw₄ : ¬p.support = ∅ ↔ ¬p.support = ∅
⊢ p.support.Nonempty ↔ p ≠ 0

Tactic:
rw [Ne, nonempty_iff_ne_empty, Ne, ← support_eq_empty]

Premises used: Ne, Finset.nonempty_iff_ne_empty, Polynomial.support_eq_empty
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
H : p ≠ 0
rw : p.coeff p.natDegree ≠ 0
⊢ p.natDegree ∈ p.support

Tactic:
rw [mem_support_iff]

Premises used: Polynomial.mem_support_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
H : p ≠ 0
⊢ p.coeff p.natDegree ≠ 0

Tactic:
(not_congr leadingCoeff_eq_zero).mpr H

Premises used: Iff.mpr, Polynomial.leadingCoeff, Polynomial.leadingCoeff_eq_zero, not_congr
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
H : p ≠ 0
⊢ p.coeff p.natDegree ≠ 0

Tactic:
exact (not_congr leadingCoeff_eq_zero).mpr H

Premises used: Iff.mpr, Polynomial.leadingCoeff_eq_zero, not_congr
-- Module: Mathlib.Algebra.Polynomial.Degree.Support
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.natDegree = p.support.max' ⋯

Tactic:
(le_max' _ _ <| natDegree_mem_support_of_nonzero h).antisymm <|
    max'_le _ _ _ le_natDegree_of_mem_supp

Premises used: Finset.max'_le, Polynomial.le_natDegree_of_mem_supp, LE.le.antisymm, Finset.le_max', Polynomial.natDegree_mem_support_of_nonzero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ WellFounded fun (p q : R[X]) ↦ p.trailingDegree < q.trailingDegree

Tactic:
InvImage.wf trailingDegree wellFounded_lt

Premises used: InvImage, wellFounded_lt, Polynomial.trailingDegree, InvImage.wf
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.TrailingMonic ↔ p.trailingCoeff = 1

Tactic:
Iff.rfl

Premises used: Polynomial.TrailingMonic, Iff.rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.TrailingMonic
⊢ p.trailingCoeff = 1

Tactic:
hp

Premises used: Polynomial.TrailingMonic
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ trailingDegree.{u} (R := R) 0 = ⊤

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.min, Polynomial.trailingDegree, Finset.inf, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (trailingCoeff 0) 0

Tactic:
rfl

Premises used: Polynomial.coeff, Polynomial.trailingCoeff, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ natTrailingDegree.{u} (R := R) 0 = 0

Tactic:
rfl

Premises used: ENat.toNat, WithTop.untopD, Polynomial.natTrailingDegree, WithTop.recTopCoe, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p = 0
⊢ p.trailingDegree = ⊤

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ p.trailingDegree = (↑p.natTrailingDegree : ℕ∞)

Tactic:
.symm <| ENat.coe_toNat <| mt trailingDegree_eq_top.1 hp

Premises used: mt, ENat.coe_toNat, Iff.mp, Eq.symm, Polynomial.trailingDegree_eq_top
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
rw : Eq (α := ℕ∞) (↑p.natTrailingDegree : ℕ∞) (↑n : ℕ∞) ↔ p.natTrailingDegree = n
rw₁ rw₂ : p.natTrailingDegree = n ↔ p.natTrailingDegree = n
⊢ p.trailingDegree = (↑n : ℕ∞) ↔ p.natTrailingDegree = n

Tactic:
rw [trailingDegree_eq_natTrailingDegree hp, Nat.cast_inj]

Premises used: Nat.cast_inj, Polynomial.trailingDegree_eq_natTrailingDegree