awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
n : ℕ
hn : (p ^ n).degree ≤ (↑n : WithBot ℕ) * a
⊢ (p ^ n * p).degree ≤ (↑n : WithBot ℕ) * a + a

Tactic:
exact degree_mul_le_of_le hn hp

Premises used: Polynomial.degree_mul_le_of_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : WithBot ℕ
b : ℕ
hp : p.degree ≤ a
zero : (HPow.hPow (β := ℕ) p 0).degree ≤ (↑0 : WithBot ℕ) * a
succ : ∀ (n : ℕ) (hn : (p ^ n).degree ≤ (↑n : WithBot ℕ) * a), (p ^ (n + 1)).degree ≤ (↑(n + 1) : WithBot ℕ) * a
⊢ (p ^ b).degree ≤ (↑b : WithBot ℕ) * a

Tactic:
induction b with
  | zero => simp [degree_one_le]
  | succ n hn =>
      rw [Nat.cast_succ, add_mul, one_mul, pow_succ]
      exact degree_mul_le_of_le hn hp

Premises used: add_mul, Nat.cast_succ, pow_succ, Polynomial.degree_one_le, one_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
pos : ∀ (ha : a = 0), leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
neg : ∀ (ha : ¬a = 0), leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
⊢ leadingCoeff ((monomial n : (a : R) → R[X]) a) = a

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
ha : a = 0
⊢ leadingCoeff ((monomial n : (a : R) → R[X]) a) = a

Tactic:
simp only [ha, (monomial n).map_zero, leadingCoeff_zero]

Premises used: Polynomial.leadingCoeff_zero, LinearMap.map_zero, Polynomial.monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
ha : ¬a = 0
neg : (if n = n then a else 0) = a
⊢ leadingCoeff ((monomial n : (a : R) → R[X]) a) = a

Tactic:
rw [leadingCoeff, natDegree_monomial, if_neg ha, coeff_monomial]

Premises used: Polynomial.leadingCoeff, Polynomial.coeff_monomial, Polynomial.natDegree_monomial, if_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ (if n = n then a else 0) = a

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
pos : ∀ (ha : a = 0), leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
neg neg₁ : ∀ (ha : ¬a = 0), leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
⊢ leadingCoeff ((monomial n : (a : R) → R[X]) a) = a

Tactic:
classical
  by_cases ha : a = 0
  · simp only [ha, (monomial n).map_zero, leadingCoeff_zero]
  · rw [leadingCoeff, natDegree_monomial, if_neg ha, coeff_monomial]
    simp

Premises used: Polynomial.leadingCoeff_zero, LinearMap.map_zero, Polynomial.monomial, Polynomial.leadingCoeff, Polynomial.coeff_monomial, Polynomial.natDegree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw : leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
rw₁ rw₂ : a = a
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).leadingCoeff = a

Tactic:
rw [C_mul_X_pow_eq_monomial, leadingCoeff_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.leadingCoeff_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).leadingCoeff = a

Tactic:
simpa only [pow_one] using leadingCoeff_C_mul_X_pow a 1

Premises used: Polynomial.leadingCoeff_C_mul_X_pow, pow_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
⊢ leadingCoeff ((C : (a : R) → R[X]) a) = a

Tactic:
leadingCoeff_monomial a 0

Premises used: Polynomial.leadingCoeff_monomial, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).leadingCoeff = 1

Tactic:
simpa only [C_1, one_mul] using leadingCoeff_C_mul_X_pow (1 : R) n

Premises used: Polynomial.C_1, Polynomial.leadingCoeff_C_mul_X_pow, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (leadingCoeff X) 1

Tactic:
simpa only [pow_one] using @leadingCoeff_X_pow R _ 1

Premises used: Polynomial.leadingCoeff_X_pow, pow_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).Monic

Tactic:
leadingCoeff_X_pow n

Premises used: Polynomial.leadingCoeff_X_pow, Polynomial.Monic
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
⊢ Monic.{u} (R := R) X

Tactic:
leadingCoeff_X

Premises used: Polynomial.leadingCoeff_X, Polynomial.Monic
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (leadingCoeff 1) 1

Tactic:
leadingCoeff_C 1

Premises used: Polynomial.leadingCoeff_C, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
⊢ Monic.{u} (R := R) 1

Tactic:
leadingCoeff_C _

Premises used: Polynomial.Monic, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
hp : Monic.{u} (R := R) 0
⊢ False

Tactic:
simp [Monic] at hp

Premises used: Polynomial.Monic
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
h : Ne.{u + 1} (α := R) 0 1
p : R[X]
hp : p.Monic
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
h : Ne.{u + 1} (α := R) 0 1
p : R[X]
hp : p.Monic
inst_1 : Nontrivial R
⊢ p ≠ 0

Tactic:
hp.ne_zero

Premises used: Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
h : Ne.{u + 1} (α := R) 0 1
p : R[X]
hp : p.Monic
inst_1 : Nontrivial R
⊢ p ≠ 0

Tactic:
exact hp.ne_zero

Premises used: Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
hc : Monic.{u} (R := R) ((C : (a : R) → R[X]) 0)
⊢ False

Tactic:
simp [Monic] at hc

Premises used: Polynomial.Monic
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q r : R[X]
hp : p.Monic
hne : q ≠ r
⊢ p ≠ 0

Tactic:
haveI := Nontrivial.of_polynomial_ne hne
  hp.ne_zero

Premises used: Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a : (p * q).degree ≤ (↑(p.natDegree + q.natDegree) : WithBot ℕ)
⊢ (p * q).natDegree ≤ p.natDegree + q.natDegree

Tactic:
apply natDegree_le_of_degree_le

Premises used: Polynomial.natDegree_le_of_degree_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a : p.degree + q.degree ≤ (↑(p.natDegree + q.natDegree) : WithBot ℕ)
⊢ (p * q).degree ≤ (↑(p.natDegree + q.natDegree) : WithBot ℕ)

Tactic:
apply le_trans (degree_mul_le p q)

Premises used: Polynomial.degree_mul_le, le_trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a : p.degree ≤ (↑p.natDegree : WithBot ℕ)
a₁ : q.degree ≤ (↑q.natDegree : WithBot ℕ)
⊢ p.degree + q.degree ≤ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)

Tactic:
apply add_le_add

Premises used: add_le_add
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ p.degree ≤ (↑p.natDegree : WithBot ℕ)

Tactic:
apply degree_le_natDegree

Premises used: Polynomial.degree_le_natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ q.degree ≤ (↑q.natDegree : WithBot ℕ)

Tactic:
apply degree_le_natDegree

Premises used: Polynomial.degree_le_natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
n m : ℕ
inst : Semiring R
p q : R[X]
hp : p.natDegree ≤ m
hg : q.natDegree ≤ n
⊢ (p * q).natDegree ≤ m + n

Tactic:
natDegree_mul_le.trans <| add_le_add ‹_› ‹_›

Premises used: add_le_add, Polynomial.natDegree_mul_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (HPow.hPow (β := ℕ) p 0).natDegree ≤ 0 * p.natDegree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : (p ^ n).natDegree ≤ n * p.natDegree
succ : (p ^ n * p).natDegree ≤ (n + 1) * p.natDegree
succ₁ : (p ^ n * p).natDegree ≤ n * p.natDegree + p.natDegree
succ₂ : (p ^ n).natDegree + p.natDegree ≤ n * p.natDegree + p.natDegree
succ₃ succ₄ : n * p.natDegree + p.natDegree ≤ n * p.natDegree + p.natDegree
⊢ (p ^ (n + 1)).natDegree ≤ (n + 1) * p.natDegree

Tactic:
grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]

Premises used: pow_succ, Nat.succ_mul, Polynomial.natDegree_mul_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).natDegree ≤ 0 * p.natDegree
succ : ∀ (n : ℕ) (ih : (p ^ n).natDegree ≤ n * p.natDegree), (p ^ (n + 1)).natDegree ≤ (n + 1) * p.natDegree
⊢ (p ^ n).natDegree ≤ n * p.natDegree

Tactic:
induction n with
  | zero => simp
  | succ n ih => grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]

Premises used: pow_succ, Nat.succ_mul, Polynomial.natDegree_mul_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
m : ℕ
inst : Semiring R
p : R[X]
n : ℕ
hp : p.natDegree ≤ m
⊢ (p ^ n).natDegree ≤ n * m

Tactic:
natDegree_pow_le.trans (Nat.mul_le_mul le_rfl ‹_›)

Premises used: le_rfl, Polynomial.natDegree_pow_le, Nat.mul_le_mul, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.natDegree ≤ 0 ↔ p.degree ≤ 0
rw₁ : p.degree ≤ (↑0 : WithBot ℕ) ↔ p.degree ≤ 0
rw₂ rw₃ : p.degree ≤ 0 ↔ p.degree ≤ 0
⊢ p.natDegree = 0 ↔ p.degree ≤ 0

Tactic:
rw [← nonpos_iff_eq_zero, natDegree_le_iff_degree_le, Nat.cast_zero]

Premises used: Nat.cast_zero, Polynomial.natDegree_le_iff_degree_le, nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
⊢ degree.{u} (R := R) 0 ≤ 0

Tactic:
natDegree_eq_zero_iff_degree_le_zero.mp rfl

Premises used: Iff.mp, Polynomial.natDegree_eq_zero_iff_degree_le_zero, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : WithBot ℕ
⊢ f.degree ≤ n ↔ ∀ (m : ℕ), n < (↑m : WithBot ℕ) → f.coeff m = 0

Tactic:
simp only [degree, Finset.max, Finset.sup_le_iff, mem_support_iff, Ne, ← not_le,
    not_imp_comm, Nat.cast_withBot]

Premises used: not_le, not_imp_comm, Polynomial.mem_support_iff, Ne, Polynomial.degree, Nat.cast_withBot, Finset.max, Finset.sup_le_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
⊢ f.degree < (↑n : WithBot ℕ) ↔ ∀ (m : ℕ), n ≤ m → f.coeff m = 0

Tactic:
simp only [degree, Finset.sup_lt_iff (WithBot.bot_lt_coe n), mem_support_iff,
    WithBot.coe_lt_coe, ← @not_le ℕ, max_eq_sup_coe, Nat.cast_withBot, Ne, not_imp_not]

Premises used: not_le, Finset.max_eq_sup_coe, Polynomial.mem_support_iff, Ne, Polynomial.degree, Finset.sup_lt_iff, WithBot.coe_lt_coe, Nat.cast_withBot, WithBot.bot_lt_coe, not_imp_not
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ 0 < p.natDegree ↔ 0 < p.degree

Tactic:
lt_iff_lt_of_le_iff_le natDegree_le_iff_degree_le

Premises used: Polynomial.natDegree_le_iff_degree_le, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
rw : degree.{u} (R := R) ((monomial n : (a : R) → R[X]) 1) = (↑n : WithBot ℕ)
rw₁ rw₂ : Eq (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
⊢ (HPow.hPow (α := R[X]) X n).degree = (↑n : WithBot ℕ)

Tactic:
rw [X_pow_eq_monomial, degree_monomial _ (one_ne_zero' R)]

Premises used: Polynomial.X_pow_eq_monomial, one_ne_zero', Polynomial.degree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).natDegree = n

Tactic:
natDegree_eq_of_degree_eq_some (degree_X_pow n)

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
⊢ (p - q).degree ≤ max p.degree q.degree

Tactic:
simpa only [degree_neg q] using degree_add_le p (-q)

Premises used: Polynomial.degree_neg, Polynomial.degree_add_le, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
a b : WithBot ℕ
hp : p.degree ≤ a
hq : q.degree ≤ b
⊢ (p - q).degree ≤ max a b

Tactic:
(p.degree_sub_le q).trans <| max_le_max ‹_› ‹_›

Premises used: max_le_max, Polynomial.degree_sub_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
⊢ (p - q).natDegree ≤ max p.natDegree q.natDegree

Tactic:
simpa only [← natDegree_neg q] using natDegree_add_le p (-q)

Premises used: Polynomial.natDegree_neg, Neg.neg, Polynomial.natDegree_add_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
n m : ℕ
inst : Ring R
p q : R[X]
hp : p.natDegree ≤ m
hq : q.natDegree ≤ n
⊢ (p - q).natDegree ≤ max m n

Tactic:
(p.natDegree_sub_le q).trans <| max_le_max ‹_› ‹_›

Premises used: max_le_max, LE.le.trans, Polynomial.natDegree_sub_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : HAdd.hAdd (α := R[X]) ((monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff : R[X]) (erase p.natDegree p) = p
hq : HAdd.hAdd (α := R[X]) ((monomial q.natDegree : (a : R) → R[X]) q.leadingCoeff : R[X]) (erase q.natDegree q) = q
rw rw₁ : WithBot.unbotD 0 q.degree = WithBot.unbotD 0 q.degree
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree

Tactic:
rw [hd]
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : HAdd.hAdd (α := R[X]) ((monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff : R[X]) (erase p.natDegree p) = p
hq : HAdd.hAdd (α := R[X]) ((monomial q.natDegree : (a : R) → R[X]) q.leadingCoeff : R[X]) (erase q.natDegree q) = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
lhs : (p - q).degree
| (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree

Tactic:
lhs
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : HAdd.hAdd (α := R[X]) ((monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff : R[X]) (erase p.natDegree p) = p
hq : HAdd.hAdd (α := R[X]) ((monomial q.natDegree : (a : R) → R[X]) q.leadingCoeff : R[X]) (erase q.natDegree q) = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
rw : (erase q.natDegree p + -erase q.natDegree q).degree
| (p - q).degree

Tactic:
rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]

Premises used: add_sub_add_left_eq_sub, sub_eq_add_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : HAdd.hAdd (α := R[X]) ((monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff : R[X]) (erase p.natDegree p) = p
hq : HAdd.hAdd (α := R[X]) ((monomial q.natDegree : (a : R) → R[X]) q.leadingCoeff : R[X]) (erase q.natDegree q) = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
rw : (erase q.natDegree p + -erase q.natDegree q).degree
| (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree

Tactic:
lhs
        rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]

Premises used: add_sub_add_left_eq_sub, sub_eq_add_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : HAdd.hAdd (α := R[X]) ((monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff : R[X]) (erase p.natDegree p) = p
hq : HAdd.hAdd (α := R[X]) ((monomial q.natDegree : (a : R) → R[X]) q.leadingCoeff : R[X]) (erase q.natDegree q) = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
conv : (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree
conv₁ : (erase q.natDegree p + -erase q.natDegree q).degree = (erase q.natDegree p + -erase q.natDegree q).degree
⊢ (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree

Tactic:
conv =>
        lhs
        rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]

Premises used: add_sub_add_left_eq_sub, sub_eq_add_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
r : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).degree ≤ 1

Tactic:
(degree_sub_le _ _).trans (max_le degree_X_le (degree_C_le.trans zero_le_one))

Premises used: Polynomial.degree_X_le, zero_le_one, Polynomial.degree_sub_le, max_le, LE.le.trans, Polynomial.degree_C_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
r : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree ≤ 1

Tactic:
natDegree_le_iff_degree_le.2 <| degree_X_sub_C_le r

Premises used: Iff.mpr, Polynomial.degree_X_sub_C_le, Polynomial.natDegree_le_iff_degree_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : p ≠ 0
hq : q ≠ 0
rw : Eq (α := WithBot ℕ) (↑(p * q).natDegree : WithBot ℕ) (↑(p.natDegree + q.natDegree) : WithBot ℕ)
rw₁ : (p * q).degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
rw₂ : (p * q).degree = HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
rw₃ : (p * q).degree = p.degree + (↑q.natDegree : WithBot ℕ)
rw₄ : (p * q).degree = p.degree + q.degree
rw₅ rw₆ : p.degree + q.degree = p.degree + q.degree
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree (mul_ne_zero hp hq),
    Nat.cast_add, ← degree_eq_natDegree hp, ← degree_eq_natDegree hq, degree_mul]

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_inj, Nat.cast_add, mul_ne_zero, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : IsDomain S
inst_3 : Module S R
inst_4 : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
pos : ∀ (hp : p = 0), (a • p).natDegree = p.natDegree
neg : ∀ (hp : ¬p = 0), (a • p).natDegree = p.natDegree
⊢ (a • p).natDegree = p.natDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : IsDomain S
inst_3 : Module S R
inst_4 : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : p = 0
⊢ (a • p).natDegree = p.natDegree

Tactic:
simp only [hp, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : IsDomain S
inst_3 : Module S R
inst_4 : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
neg : (a • p).natDegree ≤ p.natDegree
neg₁ : (a • p).coeff p.natDegree ≠ 0
⊢ (a • p).natDegree = p.natDegree

Tactic:
apply natDegree_eq_of_le_of_coeff_ne_zero

Premises used: Polynomial.natDegree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : IsDomain S
inst_3 : Module S R
inst_4 : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree ≤ p.natDegree

Tactic:
(natDegree_smul_le _ _).trans (le_refl _)

Premises used: le_refl, Polynomial.natDegree_smul_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : IsDomain S
inst_3 : Module S R
inst_4 : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).natDegree ≤ p.natDegree

Tactic:
exact (natDegree_smul_le _ _).trans (le_refl _)

Premises used: le_refl, Polynomial.natDegree_smul_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : IsDomain S
inst_3 : Module S R
inst_4 : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
neg : a • p.coeff p.natDegree ≠ 0
⊢ (a • p).coeff p.natDegree ≠ 0

Tactic:
simp only [coeff_smul]

Premises used: Polynomial.coeff_smul
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : IsDomain S
inst_3 : Module S R
inst_4 : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
neg : p.coeff p.natDegree ≠ 0
⊢ a • p.coeff p.natDegree ≠ 0

Tactic:
apply smul_ne_zero ha

Premises used: smul_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : IsDomain S
inst_3 : Module S R
inst_4 : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ p.coeff p.natDegree ≠ 0

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
n : ℕ
inl : (HPow.hPow (α := R[X]) 0 n).natDegree = n * natDegree.{u} (R := R) 0
inr : ∀ (hp : p ≠ 0), (p ^ n).natDegree = n * p.natDegree
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
obtain rfl | hp := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
n : ℕ
inl : (HPow.hPow (α := R[X]) (β := ℕ) 0 0).natDegree = 0 * natDegree.{u} (R := R) 0
inl₁ : ∀ (hn : n ≠ 0), (HPow.hPow (α := R[X]) 0 n).natDegree = n * natDegree.{u} (R := R) 0
⊢ (HPow.hPow (α := R[X]) 0 n).natDegree = n * natDegree.{u} (R := R) 0

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
⊢ (HPow.hPow (α := R[X]) (β := ℕ) 0 0).natDegree = 0 * natDegree.{u} (R := R) 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
n : ℕ
hn : n ≠ 0
⊢ (HPow.hPow (α := R[X]) 0 n).natDegree = n * natDegree.{u} (R := R) 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
rw : ¬p ^ n = 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
rw [← leadingCoeff_pow, Ne, leadingCoeff_eq_zero]

Premises used: Ne, Polynomial.leadingCoeff_pow, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ¬p ^ n = 0

Tactic:
pow_ne_zero _ hp

Premises used: pow_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ¬p ^ n = 0

Tactic:
exact pow_ne_zero _ hp

Premises used: pow_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
exact natDegree_pow' <| by
    rw [← leadingCoeff_pow, Ne, leadingCoeff_eq_zero]; exact pow_ne_zero _ hp

Premises used: Polynomial.natDegree_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
n : ℕ
inl : (HPow.hPow (α := R[X]) 0 n).natDegree = n * natDegree.{u} (R := R) 0
inr inr₁ : ∀ (hp : p ≠ 0), (p ^ n).natDegree = n * p.natDegree
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
classical
  obtain rfl | hp := eq_or_ne p 0
  · obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
  exact natDegree_pow' <| by
    rw [← leadingCoeff_pow, Ne, leadingCoeff_eq_zero]; exact pow_ne_zero _ hp

Premises used: eq_or_ne, OfNat.ofNat, rfl, Polynomial.natDegree_pow'