awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
h : #(support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) ≤ 1
ha : ¬a = 0
⊢ Eq (α := R[X])
    ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
        (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
      R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : #p.support ≤ 1
rcases :
  ∀ (n : ℕ) (a : R) (h : #(support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) ≤ 1),
    Eq (α := R[X])
      ((monomial (natDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)) : (a : R) → R[X])
          (leadingCoeff ((monomial n : (a : R) → R[X]) a)) :
        R[X])
      ((monomial n : (a : R) → R[X]) a : R[X])
⊢ (monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff = p

Tactic:
classical
  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
  by_cases ha : a = 0 <;> simp [ha]

Premises used: Iff.mp, Polynomial.card_support_le_one_iff_monomial, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Monomial
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : #p.support ≤ 1
rw : (monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff = p
rw₁ rw₂ : p = p
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) = p

Tactic:
rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.monomial_natDegree_leadingCoeff_eq_self
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ AddMonoidAlgebra.supDegree WithBot.some p.toFinsupp = p.degree

Tactic:
max_eq_sup_coe

Premises used: Finset.max_eq_sup_coe, Polynomial.degree, Finset.max, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
⊢ WellFounded fun (p q : R[X]) ↦ p.degree < q.degree

Tactic:
InvImage.wf degree wellFounded_lt

Premises used: InvImage, Polynomial.degree, wellFounded_lt, InvImage.wf
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
⊢ p.Monic

Tactic:
Subsingleton.elim _ _

Premises used: Polynomial.Monic, Subsingleton.elim
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
inst_1 : Subsingleton R
rw : degree.{u} (R := R) 0 = ⊥
rw₁ rw₂ : Eq (α := WithBot ℕ) ⊥ ⊥
⊢ p.degree = ⊥

Tactic:
rw [Subsingleton.elim p 0, degree_zero]

Premises used: Polynomial.degree_zero, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
inst_1 : Subsingleton R
rw : natDegree.{u} (R := R) 0 = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ p.natDegree = 0

Tactic:
rw [Subsingleton.elim p 0, natDegree_zero]

Premises used: Polynomial.natDegree_zero, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : p.coeff n ≠ 0
rw : (↑n : WithBot ℕ) ≤ p.degree
rw₁ : p ≠ 0
⊢ n ≤ p.natDegree

Tactic:
rw [← Nat.cast_le (α := WithBot ℕ), ← degree_eq_natDegree]

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ (↑n : WithBot ℕ) ≤ p.degree

Tactic:
le_degree_of_ne_zero h

Premises used: Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ (↑n : WithBot ℕ) ≤ p.degree

Tactic:
exact le_degree_of_ne_zero h

Premises used: Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n : ℕ
inst : Semiring R
h : Ne.{u + 1} (α := R) (coeff 0 n) 0
⊢ False

Tactic:
h rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n : ℕ
inst : Semiring R
h : Ne.{u + 1} (α := R) (coeff 0 n) 0
⊢ False

Tactic:
exact h rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
pn : p.degree ≤ (↑n : WithBot ℕ)
p1 : p.coeff n ≠ 0
⊢ p.degree = (↑n : WithBot ℕ)

Tactic:
pn.antisymm (le_degree_of_ne_zero p1)

Premises used: LE.le.antisymm, Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
p1 : p.coeff n ≠ 0
⊢ p.natDegree = n

Tactic:
pn.antisymm (le_natDegree_of_ne_zero p1)

Premises used: LE.le.antisymm, Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
pos : ∀ (hq : q = 0), p.natDegree < q.natDegree
neg : ∀ (hq : ¬q = 0), p.natDegree < q.natDegree
⊢ p.natDegree < q.natDegree

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : q = 0
⊢ p.natDegree < q.natDegree

Tactic:
(not_lt_bot <| hq ▸ hpq).elim

Premises used: False.elim, not_lt_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : q = 0
⊢ p.natDegree < q.natDegree

Tactic:
exact (not_lt_bot <| hq ▸ hpq).elim

Premises used: False.elim, not_lt_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
q : S[X]
hp : p ≠ 0
hpq : p.degree < q.degree
hq : ¬q = 0
neg : ∀ (hpq : (↑p.natDegree : WithBot ℕ) < q.degree) (hq : ¬q = 0), p.natDegree < q.natDegree
neg₁ :
  ∀ (hpq : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)) (hq : ¬q = 0),
    p.natDegree < q.natDegree
neg₂ neg₃ neg₄ neg₅ : ∀ (hpq : p.natDegree < q.natDegree) (hq : ¬q = 0), p.natDegree < q.natDegree
⊢ p.natDegree < q.natDegree

Tactic:
rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at hpq

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
q : S[X]
hpq : p.degree = q.degree
⊢ p.natDegree = q.natDegree

Tactic:
simp [natDegree, hpq]

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : p.degree < (↑n : WithBot ℕ)
⊢ p.coeff n = 0

Tactic:
Classical.not_not.1 (mt le_degree_of_ne_zero (not_le_of_gt h))

Premises used: Classical.not_not, mt, Iff.mp, Polynomial.le_degree_of_ne_zero, not_le_of_gt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
h₁ : p.degree < (↑n : WithBot ℕ)
⊢ p.coeff n = 0

Tactic:
apply coeff_eq_zero_of_degree_lt

Premises used: Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
pos : ∀ (hp : p = 0), p.degree < (↑n : WithBot ℕ)
neg : ∀ (hp : ¬p = 0), p.degree < (↑n : WithBot ℕ)
⊢ p.degree < (↑n : WithBot ℕ)

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : p = 0
pos : ∀ (h : natDegree.{u} (R := R) 0 < n), degree.{u} (R := R) 0 < (↑n : WithBot ℕ)
⊢ p.degree < (↑n : WithBot ℕ)

Tactic:
subst hp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
h : natDegree.{u} (R := R) 0 < n
⊢ degree.{u} (R := R) 0 < (↑n : WithBot ℕ)

Tactic:
WithBot.bot_lt_coe n

Premises used: Multiset.foldr, Finset.fold, Polynomial.degree, WithBot.bot_lt_coe, Finset.max, Finset.sup, List.foldr, Multiset.fold
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
h : natDegree.{u} (R := R) 0 < n
⊢ degree.{u} (R := R) 0 < (↑n : WithBot ℕ)

Tactic:
exact WithBot.bot_lt_coe n

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
neg : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑n : WithBot ℕ)
neg₁ neg₂ neg₃ neg₄ : p.natDegree < n
⊢ p.degree < (↑n : WithBot ℕ)

Tactic:
rwa [degree_eq_natDegree hp, Nat.cast_lt]

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
⊢ p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i

Tactic:
Iff.trans Polynomial.ext_iff ?_

Premises used: Polynomial.ext_iff, Iff.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
refine : (∀ (n : ℕ), p.coeff n = q.coeff n) ↔ ∀ i ≤ n, p.coeff i = q.coeff i
⊢ p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i

Tactic:
refine Iff.trans Polynomial.ext_iff ?_

Premises used: Polynomial.ext_iff, Iff.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
⊢ (∀ (n : ℕ), p.coeff n = q.coeff n) ↔ ∀ i ≤ n, p.coeff i = q.coeff i

Tactic:
forall_congr' fun i => ⟨fun h _ => h, fun h => ?_⟩

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
refine : ∀ (i : ℕ) (h : i ≤ n → p.coeff i = q.coeff i), p.coeff i = q.coeff i
⊢ (∀ (n : ℕ), p.coeff n = q.coeff n) ↔ ∀ i ≤ n, p.coeff i = q.coeff i

Tactic:
refine forall_congr' fun i => ⟨fun h _ => h, fun h => ?_⟩

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
i : ℕ
h : i ≤ n → p.coeff i = q.coeff i
⊢ p.coeff i = q.coeff i

Tactic:
(le_or_gt i n).elim h fun k => ?_

Premises used: le_or_gt, Or.elim
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
i : ℕ
h : i ≤ n → p.coeff i = q.coeff i
⊢ n < i

Tactic:
refine (le_or_gt i n).elim h fun k => ?_

Premises used: le_or_gt, Or.elim
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
i : ℕ
h : i ≤ n → p.coeff i = q.coeff i
k : n < i
⊢ p.coeff i = q.coeff i

Tactic:
(coeff_eq_zero_of_natDegree_lt (hp.trans_lt k)).trans
      (coeff_eq_zero_of_natDegree_lt (hq.trans_lt k)).symm

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, Eq.symm, LE.le.trans_lt, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n
hq : q.natDegree ≤ n
i : ℕ
h : i ≤ n → p.coeff i = q.coeff i
k : n < i
⊢ p.coeff i = q.coeff i

Tactic:
exact
    (coeff_eq_zero_of_natDegree_lt (hp.trans_lt k)).trans
      (coeff_eq_zero_of_natDegree_lt (hq.trans_lt k)).symm

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, Eq.symm, LE.le.trans_lt, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.degree ≤ (↑n : WithBot ℕ)
hq : q.degree ≤ (↑n : WithBot ℕ)
⊢ p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i

Tactic:
ext_iff_natDegree_le (natDegree_le_of_degree_le hp) (natDegree_le_of_degree_le hq)

Premises used: Polynomial.ext_iff_natDegree_le, Polynomial.natDegree_le_of_degree_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.coeff (p.natDegree + 1) = 0

Tactic:
coeff_eq_zero_of_natDegree_lt (lt_add_one _)

Premises used: lt_add_one, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
pos : ∀ (h : n < 1 + p.natDegree), p.coeff n = p.coeff n
neg : ∀ (h : ¬n < 1 + p.natDegree), 0 = p.coeff n
⊢ (if n < 1 + p.natDegree then p.coeff n else 0) = p.coeff n

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : n < 1 + p.natDegree
⊢ p.coeff n = p.coeff n

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : ¬n < 1 + p.natDegree
⊢ 0 = p.coeff n

Tactic:
(coeff_eq_zero_of_natDegree_lt (not_le.1 fun w => h (Nat.lt_one_add_iff.2 w))).symm

Premises used: not_le, Iff.mpr, Nat.lt_one_add_iff, Iff.mp, Polynomial.coeff_eq_zero_of_natDegree_lt, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : ¬n < 1 + p.natDegree
⊢ 0 = p.coeff n

Tactic:
exact (coeff_eq_zero_of_natDegree_lt (not_le.1 fun w => h (Nat.lt_one_add_iff.2 w))).symm

Premises used: not_le, Iff.mpr, Nat.lt_one_add_iff, Iff.mp, Polynomial.coeff_eq_zero_of_natDegree_lt, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p : R[X]
r : R
a : ℕ
⊢ (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).coeff (a + 1) =
    p.coeff a - p.coeff (a + 1) * r

Tactic:
simp [mul_sub]

Premises used: mul_sub
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p : R[X]
r : R
a : ℕ
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) * p).coeff (a + 1) =
    p.coeff a - r * p.coeff (a + 1)

Tactic:
simp [sub_mul]

Premises used: sub_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree < q.degree
⊢ p.coeff q.natDegree = 0

Tactic:
coeff_eq_zero_of_degree_lt (lt_of_lt_of_le h degree_le_natDegree)

Premises used: Polynomial.degree_le_natDegree, lt_of_lt_of_le, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : WithBot ℕ
h : n < p.degree
⊢ p ≠ 0

Tactic:
mt degree_eq_bot.2 h.ne_bot

Premises used: Iff.mpr, mt, Polynomial.degree_eq_bot, LT.lt.ne_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hpq : p.degree ≤ q.degree
hp : p ≠ 0
rwa : ¬p.degree = ⊥
rwa₁ rwa₂ rwa₃ rwa₄ : ¬p = 0
⊢ p.degree ≠ ⊥

Tactic:
rwa [Ne, Polynomial.degree_eq_bot]

Premises used: Ne, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natDegree
H : p = 0
⊢ False

Tactic:
simp [H] at h
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
pos : ∀ (hp : p = 0), p.degree < q.degree
neg : ∀ (hp : ¬p = 0), p.degree < q.degree
⊢ p.degree < q.degree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
pos : ⊥ < q.degree
⊢ p.degree < q.degree

Tactic:
simp only [hp, degree_zero]

Premises used: Polynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
pos : q.degree ≠ ⊥
⊢ ⊥ < q.degree

Tactic:
rw [bot_lt_iff_ne_bot]

Premises used: bot_lt_iff_ne_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : p = 0
hq : q.degree = ⊥
⊢ False

Tactic:
simp [hp, degree_eq_bot.mp hq] at h

Premises used: Iff.mp, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
hp : ¬p = 0
neg : (↑p.natDegree : WithBot ℕ) < q.degree
neg₁ : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
neg₂ neg₃ neg₄ neg₅ : p.natDegree < q.natDegree
⊢ p.degree < q.degree

Tactic:
rwa [degree_eq_natDegree hp, degree_eq_natDegree <| ne_zero_of_natDegree_gt h, Nat.cast_lt]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.ne_zero_of_natDegree_gt, Nat.cast_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
⊢ q ≠ 0

Tactic:
have hq : q ≠ 0 := ne_zero_of_degree_gt h
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
hq : q ≠ 0
rwa : ∀ (h : (↑p.natDegree : WithBot ℕ) < q.degree) (hq : q ≠ 0), p.natDegree < q.natDegree
rwa₁ :
  ∀ (h : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)) (hq : q ≠ 0),
    p.natDegree < q.natDegree
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : p.natDegree < q.natDegree) (hq : q ≠ 0), p.natDegree < q.natDegree
⊢ p.natDegree < q.natDegree

Tactic:
rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 0
a : p.coeff 0 = coeff ((C : (a : R) → R[X]) (p.coeff 0)) 0
a₁ : ∀ (n : ℕ), p.coeff (n + 1) = coeff ((C : (a : R) → R[X]) (p.coeff 0)) (n + 1)
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
ext (_ | n)
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 0
⊢ p.coeff 0 = coeff ((C : (a : R) → R[X]) (p.coeff 0)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
a : p.degree < (↑(n + 1) : WithBot ℕ)
⊢ p.coeff (n + 1) = coeff ((C : (a : R) → R[X]) (p.coeff 0)) (n + 1)

Tactic:
rw [coeff_C, if_neg (Nat.succ_ne_zero _), coeff_eq_zero_of_degree_lt]

Premises used: Polynomial.coeff_C, Nat.succ_ne_zero, if_neg, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.degree < (↑(n + 1) : WithBot ℕ)

Tactic:
h.trans_lt (WithBot.coe_lt_coe.2 n.succ_pos)

Premises used: Iff.mpr, WithBot.coe_lt_coe, Nat.succ_pos, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.degree < (↑(n + 1) : WithBot ℕ)

Tactic:
exact h.trans_lt (WithBot.coe_lt_coe.2 n.succ_pos)

Premises used: Iff.mpr, WithBot.coe_lt_coe, Nat.succ_pos, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree = 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
eq_C_of_degree_le_zero h.le

Premises used: Eq.le, Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.degree ≤ 0 ↔ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
⟨eq_C_of_degree_le_zero, fun h => h.symm ▸ degree_C_le⟩

Premises used: Eq.rec, Polynomial.eq_C_of_degree_le_zero, Iff.intro, Eq.symm, Polynomial.degree_C_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.degree < p.degree
rw : p.coeff p.natDegree ≠ 0
⊢ (p + q).coeff p.natDegree ≠ 0

Tactic:
rw [coeff_add, coeff_natDegree_eq_zero_of_degree_lt h, add_zero]

Premises used: Polynomial.coeff_add, add_zero, Polynomial.coeff_natDegree_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ p.coeff p.natDegree ≠ 0

Tactic:
mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)

Premises used: Polynomial.ne_zero_of_degree_gt, mt, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ p.coeff p.natDegree ≠ 0

Tactic:
exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)

Premises used: Polynomial.ne_zero_of_degree_gt, mt, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree < q.degree
rw : (q + p).degree = q.degree
rw₁ rw₂ : q.degree = q.degree
⊢ (p + q).degree = q.degree

Tactic:
rw [add_comm, degree_add_eq_left_of_degree_lt h]

Premises used: Polynomial.degree_add_eq_left_of_degree_lt, add_comm
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (p + q).natDegree = p.natDegree

Tactic:
natDegree_eq_of_degree_eq (degree_add_eq_left_of_degree_lt h)

Premises used: Polynomial.degree_add_eq_left_of_degree_lt, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.natDegree < p.natDegree
⊢ (p + q).natDegree = p.natDegree

Tactic:
natDegree_add_eq_left_of_degree_lt (degree_lt_degree h)

Premises used: Polynomial.natDegree_add_eq_left_of_degree_lt, Polynomial.degree_lt_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree < q.degree
⊢ (p + q).natDegree = q.natDegree

Tactic:
natDegree_eq_of_degree_eq (degree_add_eq_right_of_degree_lt h)

Premises used: Polynomial.degree_add_eq_right_of_degree_lt, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.natDegree < q.natDegree
⊢ (p + q).natDegree = q.natDegree

Tactic:
natDegree_add_eq_right_of_degree_lt (degree_lt_degree h)

Premises used: Polynomial.natDegree_add_eq_right_of_degree_lt, Polynomial.degree_lt_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
inl :
  (HAdd.hAdd (α := R[X]) (β := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) a : R[X])).natDegree = natDegree.{u} (R := R) 0
inr : ∀ (hp : p ≠ 0), (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
a : R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) a : R[X])).natDegree = natDegree.{u} (R := R) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
pos : ∀ (hpd : p.degree ≤ 0), (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
neg : ∀ (hpd : 0 < p.degree), (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree

Tactic:
by_cases! hpd : p.degree ≤ 0

Premises used: Polynomial.degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
pos :
  (HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
        ((C : (a : R) → R[X]) a : R[X])).natDegree =
    natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
pos₁ :
  natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0 + a)) =
    natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
pos₂ : 0 = natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0))
pos₃ pos₄ : Eq (α := ℕ) 0 0
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree

Tactic:
rw [eq_C_of_degree_le_zero hpd, ← C_add, natDegree_C, natDegree_C]

Premises used: Polynomial.natDegree_C, Polynomial.eq_C_of_degree_le_zero, Polynomial.C_add