awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)

Premises used: mt, Iff.mp, mul_ne_zero, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)

Premises used: mt, Iff.mp, mul_ne_zero, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
⊢ Eq.{u + 1} (α := R) (leadingCoeff 1) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
⊢ (leadingCoeffHom : (a : R[X]) → R) p = p.leadingCoeff

Tactic:
rfl

Premises used: Polynomial.leadingCoeff, Polynomial.coeff, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
n : ℕ
⊢ (p ^ n).leadingCoeff = p.leadingCoeff ^ n

Tactic:
(leadingCoeffHom : R[X] →* R).map_pow p n

Premises used: Polynomial.leadingCoeffHom, Polynomial.leadingCoeff, Polynomial.coeff, MonoidHom.map_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
a p : R[X]
hap : a ∣ p
⊢ a.leadingCoeff ∣ p.leadingCoeff

Tactic:
map_dvd leadingCoeffHom hap

Premises used: Polynomial.leadingCoeffHom, Polynomial.leadingCoeff, Polynomial.coeff, map_dvd
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
inl : degree.{u} (R := R) 0 ≤ (0 * q).degree
inr : ∀ (hp : p ≠ 0), p.degree ≤ (p * q).degree
⊢ p.degree ≤ (p * q).degree

Tactic:
obtain rfl | hp := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
q : R[X]
hq : q ≠ 0
⊢ degree.{u} (R := R) 0 ≤ (0 * q).degree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
inr : (↑p.natDegree : WithBot ℕ) ≤ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ p.degree ≤ (p * q).degree

Tactic:
rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ (↑p.natDegree : WithBot ℕ) ≤ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)

Tactic:
WithBot.coe_le_coe.2 (Nat.le_add_right _ _)

Premises used: Iff.mpr, WithBot.some, Nat.le_add_right, WithBot.coe_le_coe, WithBot.map₂, Option.map₂
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ (↑p.natDegree : WithBot ℕ) ≤ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)

Tactic:
exact WithBot.coe_le_coe.2 (Nat.le_add_right _ _)

Premises used: Iff.mpr, Nat.le_add_right, WithBot.coe_le_coe
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
inl : degree.{u} (R := R) 0 ≤ (0 * q).degree
inr inr₁ : ∀ (hp : p ≠ 0), p.degree ≤ (p * q).degree
⊢ p.degree ≤ (p * q).degree

Tactic:
classical
  obtain rfl | hp := eq_or_ne p 0
  · simp
  · rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]
    exact WithBot.coe_le_coe.2 (Nat.le_add_right _ _)

Premises used: Iff.mpr, Polynomial.degree_eq_natDegree, Nat.le_add_right, WithBot.coe_le_coe, eq_or_ne, OfNat.ofNat, rfl, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
hp : p.Monic
⊢ 0 < p.natDegree ↔ p ≠ 1

Tactic:
Nat.pos_iff_ne_zero.trans hp.natDegree_eq_zero.not

Premises used: Polynomial.Monic.natDegree_eq_zero, Nat.pos_iff_ne_zero, Iff.not, Iff.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
hp : p.Monic
⊢ 0 < p.degree ↔ p ≠ 1

Tactic:
natDegree_pos_iff_degree_pos.symm.trans hp.natDegree_pos

Premises used: Iff.trans, Polynomial.Monic.natDegree_pos, Polynomial.natDegree_pos_iff_degree_pos, Iff.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
n : ℕ
hn : 0 < n
r : R
rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-r) : R[X])).leadingCoeff = 1
rw₂ rw₃ : Eq.{u + 1} (α := R) 1 1
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1

Tactic:
rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_pow_add_C hn]

Premises used: Polynomial.C, Polynomial.leadingCoeff_X_pow_add_C, sub_eq_add_neg, map_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
n : ℕ
hn : 0 < n
⊢ (HPow.hPow (α := R[X]) X n - 1).leadingCoeff = 1

Tactic:
leadingCoeff_X_pow_sub_C hn

Premises used: Polynomial.leadingCoeff_X_pow_sub_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
a : R
rw : (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) a : R[X])).degree = 1
rw₁ : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-a) : R[X])).degree = 1
rw₂ rw₃ : Eq (α := WithBot ℕ) 1 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree = 1

Tactic:
rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]

Premises used: Polynomial.C, sub_eq_add_neg, map_neg, Polynomial.degree_X_add_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
x : R
rw : natDegree.{u} (R := R) X = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1

Tactic:
rw [natDegree_sub_C, natDegree_X]

Premises used: Polynomial.natDegree_X, Polynomial.natDegree_sub_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
S : Type v
inst : Ring S
c : S
rw : (HAdd.hAdd (α := S[X]) (β := S[X]) X (-(C : (a : S) → S[X]) c : S[X])).nextCoeff = -c
rw₁ : (HAdd.hAdd (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) (-c) : S[X])).nextCoeff = -c
rw₂ rw₃ : -c = -c
⊢ (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) c : S[X])).nextCoeff = -c

Tactic:
rw [sub_eq_add_neg, ← map_neg C c, nextCoeff_X_add_C]

Premises used: Polynomial.C, sub_eq_add_neg, Polynomial.nextCoeff_X_add_C, map_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
hn : 0 < n
a : R
rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-a) : R[X])).degree = (↑n : WithBot ℕ)
rw₂ rw₃ : Eq (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)

Tactic:
rw [sub_eq_add_neg, ← map_neg C a, degree_X_pow_add_C hn]

Premises used: Polynomial.C, Polynomial.degree_X_pow_add_C, sub_eq_add_neg, map_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
hn : 0 < n
a : R
rw : HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-a) : R[X]) ≠ 0
⊢ HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) ≠ 0

Tactic:
rw [sub_eq_add_neg, ← map_neg C a]

Premises used: Polynomial.C, sub_eq_add_neg, map_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-a) : R[X]) ≠ 0

Tactic:
X_pow_add_C_ne_zero hn _

Premises used: Polynomial.X_pow_add_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-a) : R[X]) ≠ 0

Tactic:
exact X_pow_add_C_ne_zero hn _

Premises used: Polynomial.X_pow_add_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
r : R
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ≠ 0

Tactic:
pow_one (X : R[X]) ▸ X_pow_sub_C_ne_zero zero_lt_one r

Premises used: Eq.rec, zero_lt_one, pow_one, Polynomial.X, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
α : Type u_1
m : Multiset α
f : α → R
⊢ 0 ∉ Multiset.map (fun (a : α) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) m

Tactic:
fun mem =>
  let ⟨_a, _, ha⟩ := Multiset.mem_map.mp mem
  X_sub_C_ne_zero _ ha

Premises used: False, Multiset.mem_map, _private.0.Polynomial.zero_notMem_multiset_map_X_sub_C.match_1, Iff.mp, Polynomial.X_sub_C_ne_zero, Not
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
r : R
rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) r : R[X])).natDegree = n
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-r) : R[X])).natDegree = n
rw₂ rw₃ : n = n
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree = n

Tactic:
rw [sub_eq_add_neg, ← map_neg C r, natDegree_X_pow_add_C]

Premises used: Polynomial.C, sub_eq_add_neg, map_neg, Polynomial.natDegree_X_pow_add_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
S : Type v
inst : Ring S
r : S
rw : (HAdd.hAdd (α := S[X]) (β := S[X]) X (-(C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
rw₁ : (HAdd.hAdd (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) (-r) : S[X])).leadingCoeff = 1
rw₂ rw₃ : Eq.{v + 1} (α := S) 1 1
⊢ (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1

Tactic:
rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_add_C]

Premises used: Polynomial.C, sub_eq_add_neg, map_neg, Polynomial.leadingCoeff_X_add_C
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 1
n : ℕ
⊢ p.coeff Nat.zero =
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      Nat.zero

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 1
n_1 n : ℕ
⊢ p.coeff Nat.zero.succ =
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      Nat.zero.succ

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 1
n_1 n m : ℕ
⊢ p.degree < (↑m.succ.succ : WithBot ℕ)

Tactic:
have : degree p < m.succ.succ := lt_of_le_of_lt h Nat.one_lt_ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 1
n_1 n m : ℕ
this : p.degree < (↑m.succ.succ : WithBot ℕ)
⊢ p.coeff m.succ.succ =
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      m.succ.succ

Tactic:
simp [coeff_eq_zero_of_degree_lt this]

Premises used: Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree = 1
⊢ p.degree = (↑1 : WithBot ℕ)

Tactic:
rw [← Nat.cast_one] at h

Premises used: Nat.cast_one
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree = (↑1 : WithBot ℕ)
rw :
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₁ rw₂ :
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
⊢ HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])

Tactic:
rw [leadingCoeff, natDegree_eq_of_degree_eq_some h]

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.natDegree ≤ 1
⊢ p =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])

Tactic:
eq_X_add_C_of_degree_le_one <| degree_le_of_natDegree_le h

Premises used: Polynomial.eq_X_add_C_of_degree_le_one, Polynomial.degree_le_of_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
rw : p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) 1 X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₁ :
  p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 1) X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₂ :
  p =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₃ :
  p =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₄ rw₅ : p = p
⊢ p = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (p.coeff 0) : R[X])

Tactic:
rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]

Premises used: Polynomial.C_1, Polynomial.eq_X_add_C_of_natDegree_le_one, Eq.le, Polynomial.Monic.coeff_natDegree, Polynomial.X, one_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.natDegree ≤ 1
⊢ ∃ (a : R) (b : R),
    p =
      HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])

Tactic:
⟨p.coeff 1, p.coeff 0, eq_X_add_C_of_natDegree_le_one h⟩

Premises used: Polynomial.eq_X_add_C_of_natDegree_le_one, Polynomial.coeff, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : ¬p.degree < 0 ↔ p ≠ 0
rw₁ : ¬p.degree = ⊥ ↔ p ≠ 0
rw₂ rw₃ : ¬p = 0 ↔ p ≠ 0
⊢ 0 ≤ p.degree ↔ p ≠ 0

Tactic:
rw [← not_lt, Nat.WithBot.lt_zero_iff, degree_eq_bot]

Premises used: Nat.WithBot.lt_zero_iff, not_lt, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hdeg : (↑n : WithBot ℕ) ≤ p.degree
⊢ p ≠ 0

Tactic:
zero_le_degree_iff.mp <| (WithBot.coe_le_coe.mpr n.zero_le).trans hdeg

Premises used: Iff.mpr, Nat.zero_le, Polynomial.zero_le_degree_iff, WithBot.coe_le_coe, Iff.mp, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hdeg : (↑n : WithBot ℕ) ≤ p.degree
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hdeg : LE.le (α := WithBot ℕ) (↑n : WithBot ℕ) (↑p.natDegree : WithBot ℕ)),
    (↑n : WithBot ℕ) ≤ (↑p.natDegree : WithBot ℕ)
⊢ (↑n : WithBot ℕ) ≤ (↑p.natDegree : WithBot ℕ)

Tactic:
rwa [degree_eq_natDegree <| ne_zero_of_coe_le_degree hdeg] at hdeg

Premises used: Polynomial.degree_eq_natDegree, Polynomial.ne_zero_of_coe_le_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b : R
inst : Semiring R
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).degree ≤
    1

Tactic:
degree_add_le_of_degree_le (degree_C_mul_X_le _) <| le_trans degree_C_le Nat.WithBot.coe_nonneg

Premises used: Polynomial.degree_C_mul_X_le, Polynomial.degree_add_le_of_degree_le, Nat.WithBot.coe_nonneg, le_trans, Polynomial.degree_C_le
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b : R
inst : Semiring R
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).degree <
    2

Tactic:
degree_linear_le.trans_lt <| WithBot.coe_lt_coe.mpr one_lt_two

Premises used: Iff.mpr, WithBot.coe_lt_coe, one_lt_two, Polynomial.degree_linear_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
rw : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).degree = 1
rw₁ rw₂ : Eq (α := WithBot ℕ) 1 1
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).degree =
    1

Tactic:
rw [degree_add_eq_left_of_degree_lt <| degree_C_lt_degree_C_mul_X ha, degree_C_mul_X ha]

Premises used: Polynomial.degree_C_lt_degree_C_mul_X, Polynomial.degree_add_eq_left_of_degree_lt, Polynomial.degree_C_mul_X
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b : R
inst : Semiring R
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1

Tactic:
natDegree_le_of_degree_le degree_linear_le

Premises used: Polynomial.natDegree_le_of_degree_le, Polynomial.degree_linear_le
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
rw : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1

Tactic:
rw [natDegree_add_C, natDegree_C_mul_X a ha]

Premises used: Polynomial.natDegree_C_mul_X, Polynomial.natDegree_add_C
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) b : R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)).leadingCoeff =
    a
rw₁ : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).leadingCoeff = a
rw₂ rw₃ : a = a
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff =
    a

Tactic:
rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_lt_degree_C_mul_X ha),
    leadingCoeff_C_mul_X]

Premises used: Polynomial.degree_C_lt_degree_C_mul_X, add_comm, Polynomial.leadingCoeff_C_mul_X, Polynomial.leadingCoeff_add_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c : 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 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).degree ≤
    2

Tactic:
simpa only [add_assoc] using
    degree_add_le_of_degree_le (degree_C_mul_X_pow_le 2 a)
      (le_trans degree_linear_le <| WithBot.coe_le_coe.mpr one_le_two)

Premises used: Iff.mpr, add_assoc, Polynomial.degree_C_mul_X_pow_le, WithBot.coe_le_coe, one_le_two, Polynomial.degree_linear_le, Polynomial.degree_add_le_of_degree_le, OfNat.ofNat, le_trans
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c : 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 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).degree <
    3

Tactic:
degree_quadratic_le.trans_lt <| WithBot.coe_lt_coe.mpr <| lt_add_one 2

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

Tactic:
simpa only [degree_C_mul_X_pow 2 ha] using degree_linear_lt

Premises used: OfNat.ofNat, Polynomial.degree_C_mul_X_pow, Polynomial.degree_linear_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c : R
inst : Semiring R
ha : a ≠ 0
rw : Eq (α := WithBot ℕ) (↑2 : WithBot ℕ) 2
⊢ (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])).degree =
    2

Tactic:
rw [add_assoc, degree_add_eq_left_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    degree_C_mul_X_pow 2 ha]

Premises used: add_assoc, Polynomial.degree_add_eq_left_of_degree_lt, Polynomial.degree_linear_lt_degree_C_mul_X_sq, OfNat.ofNat, Polynomial.degree_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c : R
inst : Semiring R
ha : a ≠ 0
⊢ Eq (α := WithBot ℕ) (↑2 : WithBot ℕ) 2

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c : 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 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).natDegree ≤
    2

Tactic:
natDegree_le_of_degree_le degree_quadratic_le

Premises used: Polynomial.degree_quadratic_le, Polynomial.natDegree_le_of_degree_le
-- Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree
Goal:
R : Type u
a b c : 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 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).natDegree =
    2

Tactic:
natDegree_eq_of_degree_eq_some <| degree_quadratic ha

Premises used: Polynomial.degree_quadratic, Polynomial.natDegree_eq_of_degree_eq_some