awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
i : ℕ
r : R
pos : ∀ (hr : r = 0), natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = 0
neg : ∀ (hr : ¬r = 0), natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = i
⊢ natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = if r = 0 then 0 else i

Tactic:
split_ifs with hr
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
i : ℕ
r : R
hr : r = 0
⊢ natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = 0

Tactic:
simp [hr]
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
i : ℕ
r : R
hr : ¬r = 0
neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X i)).natDegree = i
neg₁ neg₂ : i = i
⊢ natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = i

Tactic:
rw [← C_mul_X_pow_eq_monomial, natDegree_C_mul_X_pow i r hr]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.natDegree_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
rw : (if a = 0 then 0 else m) ≤ m
⊢ natDegree.{u} (R := R) ((monomial m : (a : R) → R[X]) a) ≤ m

Tactic:
rw [Polynomial.natDegree_monomial]

Premises used: Polynomial.natDegree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
pos : a = 0 → 0 ≤ m
neg : ¬a = 0 → m ≤ m
⊢ (if a = 0 then 0 else m) ≤ m

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
h : a = 0
⊢ 0 ≤ m

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
h : ¬a = 0
⊢ m ≤ m

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
h : a = 0
⊢ 0 ≤ m

Tactic:
exacts [Nat.zero_le _, le_rfl]

Premises used: Nat.zero_le, le_rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
rw rw₁ rw₂ : (if a = 0 then 0 else m) ≤ m
pos : a = 0 → 0 ≤ m
neg : ¬a = 0 → m ≤ m
⊢ natDegree.{u} (R := R) ((monomial m : (a : R) → R[X]) a) ≤ m

Tactic:
classical
  rw [Polynomial.natDegree_monomial]
  split_ifs
  exacts [Nat.zero_le _, le_rfl]

Premises used: Nat.zero_le, le_rfl, Polynomial.natDegree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
i : ℕ
r : R
r0 : r ≠ 0
⊢ natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = i

Tactic:
letI := Classical.decEq R
  Eq.trans (natDegree_monomial _ _) (if_neg r0)

Premises used: Polynomial.natDegree_monomial, if_neg, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hn : p.degree = (↑n : WithBot ℕ)
⊢ p.coeff n ≠ 0

Tactic:
fun h =>
  mem_support_iff.mp (mem_of_max hn) h

Premises used: Polynomial.mem_support_iff, Finset.mem_of_max, Iff.mp, Not
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).degree ≤ (↑n : WithBot ℕ)

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

Premises used: Polynomial.C_1, Polynomial.degree_C_mul_X_pow_le, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
⊢ degree.{u} (R := R) X ≤ 1

Tactic:
degree_monomial_le _ _

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

Tactic:
natDegree_le_of_degree_le degree_X_le

Premises used: Polynomial.degree_X_le, Polynomial.natDegree_le_of_degree_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
rw : WithBot.succ (↑p.natDegree : WithBot ℕ) = p.natDegree + 1
⊢ p.degree.succ = p.natDegree + 1

Tactic:
rw [degree_eq_natDegree h]

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
⊢ WithBot.succ (↑p.natDegree : WithBot ℕ) = p.natDegree + 1

Tactic:
WithBot.succ_coe p.natDegree

Premises used: Order.succ, WithBot.succ_coe, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
⊢ WithBot.succ (↑p.natDegree : WithBot ℕ) = p.natDegree + 1

Tactic:
exact WithBot.succ_coe p.natDegree

Premises used: WithBot.succ_coe, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ degree.{u} (R := R) 1 = 0

Tactic:
degree_C one_ne_zero

Premises used: Polynomial.degree_C, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ degree.{u} (R := R) X = 1

Tactic:
degree_monomial _ one_ne_zero

Premises used: one_ne_zero, Polynomial.X, Polynomial.degree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ natDegree.{u} (R := R) X = 1

Tactic:
natDegree_eq_of_degree_eq_some degree_X

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_X
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
rw rw₁ : p.support.max = p.support.max
⊢ (-p).support.max = p.support.max

Tactic:
rw [support_neg]

Premises used: Polynomial.support_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
a : WithBot ℕ
p : R[X]
hp : p.degree ≤ a
⊢ (-p).degree ≤ a

Tactic:
p.degree_neg.le.trans hp

Premises used: Eq.le, Polynomial.degree_neg, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ (-p).natDegree = p.natDegree

Tactic:
simp [natDegree]

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
m : ℕ
inst : Ring R
p : R[X]
hp : p.natDegree ≤ m
⊢ (-p).natDegree ≤ m

Tactic:
(natDegree_neg p).le.trans hp

Premises used: Eq.le, Polynomial.natDegree_neg, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
n : ℤ
rw : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (↑n : R)) = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ natDegree.{u} (R := R) (↑n : R[X]) = 0

Tactic:
rw [← C_eq_intCast, natDegree_C]

Premises used: Polynomial.C_eq_intCast, Polynomial.natDegree_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
n : ℤ
⊢ natDegree.{u} (R := R) (↑n : R[X]) ≤ Zero.zero

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
rw : (-p).coeff (-p).natDegree = -p.leadingCoeff
rw₁ : (-p).coeff (-p).natDegree = -p.coeff p.natDegree
rw₂ : (-p).coeff p.natDegree = -p.coeff p.natDegree
rw₃ rw₄ : -p.coeff p.natDegree = -p.coeff p.natDegree
⊢ (-p).leadingCoeff = -p.leadingCoeff

Tactic:
rw [leadingCoeff, leadingCoeff, natDegree_neg, coeff_neg]

Premises used: Polynomial.leadingCoeff, Polynomial.coeff_neg, Polynomial.natDegree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
simp :
  ¬p.natDegree = 0 → p.coeff (p.natDegree - 1) = 0 ↔ ¬p.natDegree = 0 → ¬p.natDegree = 0 ∧ p.coeff (p.natDegree - 1) = 0
⊢ p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0

Tactic:
simp [nextCoeff, or_iff_not_imp_left, pos_iff_ne_zero]

Premises used: Polynomial.nextCoeff, Classical.or_iff_not_imp_left, pos_iff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ ¬p.natDegree = 0 → p.coeff (p.natDegree - 1) = 0 ↔ ¬p.natDegree = 0 → ¬p.natDegree = 0 ∧ p.coeff (p.natDegree - 1) = 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.nextCoeff ≠ 0 ↔ p.natDegree ≠ 0 ∧ p.coeff (p.natDegree - 1) ≠ 0

Tactic:
simp [nextCoeff]

Premises used: Polynomial.nextCoeff
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
c : R
⊢ Eq.{u + 1} (α := R)
    (if natDegree.{u} (R := R) ((C : (a : R) → R[X]) c) = 0 then 0
    else coeff ((C : (a : R) → R[X]) c) (natDegree.{u} (R := R) ((C : (a : R) → R[X]) c) - 1))
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : 0 < p.natDegree
hnc : ¬p.natDegree = 0
⊢ p.nextCoeff = p.coeff (p.natDegree - 1)

Tactic:
rw [nextCoeff, if_neg]

Premises used: Polynomial.nextCoeff, if_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : 0 < p.natDegree
hnc : ∀ (hp : p.natDegree = 0), p.natDegree ≤ 0
⊢ ¬p.natDegree = 0

Tactic:
contrapose! hp
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ p.natDegree ≤ 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (p + q).degree ≤ max p.degree q.degree

Tactic:
simpa only [degree, ← support_toFinsupp, toFinsupp_add]
    using AddMonoidAlgebra.sup_support_add_le _ _ _

Premises used: Polynomial.degree, Polynomial.toFinsupp_add, AddMonoidAlgebra.sup_support_add_le, Polynomial.support_toFinsupp
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.degree ≤ (↑n : WithBot ℕ)
hq : q.degree ≤ (↑n : WithBot ℕ)
⊢ (p + q).degree ≤ (↑n : WithBot ℕ)

Tactic:
(degree_add_le p q).trans <| max_le hp hq

Premises used: max_le, Polynomial.degree_add_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring 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_add_le q).trans <| max_le_max ‹_› ‹_›

Premises used: max_le_max, Polynomial.degree_add_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inl : ∀ (h : (p + q).degree ≤ p.degree), (p + q).natDegree ≤ max p.natDegree q.natDegree
inr : ∀ (h : (p + q).degree ≤ q.degree), (p + q).natDegree ≤ max p.natDegree q.natDegree
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree

Tactic:
rcases le_max_iff.1 (degree_add_le p q) with h | h

Premises used: Iff.mp, Polynomial.degree_add_le, le_max_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : (p + q).degree ≤ p.degree
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree

Tactic:
simp [natDegree_le_natDegree h]

Premises used: Polynomial.natDegree_le_natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : (p + q).degree ≤ q.degree
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree

Tactic:
simp [natDegree_le_natDegree h]

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

Tactic:
(natDegree_add_le p q).trans <| max_le hp hq

Premises used: max_le, LE.le.trans, Polynomial.natDegree_add_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
n m : ℕ
inst : Semiring R
p q : R[X]
hp : p.natDegree ≤ m
hq : q.natDegree ≤ n
⊢ (p + q).natDegree ≤ max m n

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

Premises used: max_le_max, LE.le.trans, Polynomial.natDegree_add_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (leadingCoeff 0) 0

Tactic:
rfl

Premises used: Polynomial.leadingCoeff, Polynomial.coeff, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.leadingCoeff = 0 ↔ p = 0

Tactic:
⟨fun h =>
    Classical.by_contradiction fun hp =>
      mt mem_support_iff.1 (Classical.not_not.2 h) (mem_of_max (degree_eq_natDegree hp)),
    fun h => h.symm ▸ leadingCoeff_zero⟩

Premises used: Iff.mpr, Polynomial.degree_eq_natDegree, Classical.not_not, Polynomial.leadingCoeff_zero, Classical.by_contradiction, mt, Eq.rec, Polynomial.mem_support_iff, Finset.mem_of_max, Iff.intro, Iff.mp, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : ¬p.leadingCoeff = 0 ↔ p ≠ 0
rw₁ rw₂ : ¬p = 0 ↔ p ≠ 0
⊢ p.leadingCoeff ≠ 0 ↔ p ≠ 0

Tactic:
rw [Ne, leadingCoeff_eq_zero]

Premises used: Ne, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p = 0 ↔ p.degree = ⊥
rw₁ rw₂ : p = 0 ↔ p = 0
⊢ p.leadingCoeff = 0 ↔ p.degree = ⊥

Tactic:
rw [leadingCoeff_eq_zero, degree_eq_bot]

Premises used: Polynomial.leadingCoeff_eq_zero, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree ≤ n

Tactic:
natDegree_le_iff_degree_le.2 <| degree_C_mul_X_pow_le _ _

Premises used: Iff.mpr, Polynomial.degree_C_mul_X_pow_le, Polynomial.natDegree_le_iff_degree_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
simp : (Finsupp.erase n p.toFinsupp).support.max ≤ p.toFinsupp.support.max
⊢ (erase n p).degree ≤ p.degree

Tactic:
simp only [erase_def, AddMonoidAlgebra.erase, AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff,
    degree, support]

Premises used: AddMonoidAlgebra.coeff, Polynomial.degree, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.erase, Polynomial.support, Polynomial.erase_def
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : (Finsupp.erase n p.toFinsupp).support ⊆ p.toFinsupp.support
⊢ (Finsupp.erase n p.toFinsupp).support.max ≤ p.toFinsupp.support.max

Tactic:
apply sup_mono

Premises used: Finset.sup_mono
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (Finsupp.erase n p.toFinsupp).support ⊆ p.toFinsupp.support

Tactic:
simpa using Finset.erase_subset ..

Premises used: Finset.erase_subset
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
apply : (erase p.natDegree p).degree ≠ p.degree
⊢ (erase p.natDegree p).degree < p.degree

Tactic:
apply lt_of_le_of_ne (degree_erase_le _ _)

Premises used: Polynomial.degree_erase_le, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
rw : (p.support.erase p.natDegree).max ≠ (↑p.natDegree : WithBot ℕ)
⊢ (erase p.natDegree p).degree ≠ p.degree

Tactic:
rw [degree_eq_natDegree hp, degree, support_erase]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.degree, Polynomial.support_erase
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ (p.support.erase p.natDegree).max ≠ (↑p.natDegree : WithBot ℕ)

Tactic:
fun h => notMem_erase _ _ (mem_of_max h)

Premises used: Finset.mem_of_max, Finset.notMem_erase, Polynomial.natDegree, Polynomial.support, Not
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ (p.support.erase p.natDegree).max ≠ (↑p.natDegree : WithBot ℕ)

Tactic:
exact fun h => notMem_erase _ _ (mem_of_max h)

Premises used: Finset.mem_of_max, Finset.notMem_erase
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
rw : (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
⊢ (p.update n a).degree ≤ max p.degree (↑n : WithBot ℕ)

Tactic:
rw [degree, support_update]

Premises used: Polynomial.degree, Polynomial.support_update
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
pos : a = 0 → (p.support.erase n).max ≤ max p.degree (↑n : WithBot ℕ)
neg : ¬a = 0 → (insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
⊢ (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
h : a = 0
⊢ (p.support.erase n).max ≤ max p.degree (↑n : WithBot ℕ)

Tactic:
(Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)

Premises used: Finset.max_mono, LE.le.trans, le_max_left, Finset.erase_subset
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
h : a = 0
⊢ (p.support.erase n).max ≤ max p.degree (↑n : WithBot ℕ)

Tactic:
exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)

Premises used: Finset.max_mono, LE.le.trans, Finset.erase_subset
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
h : ¬a = 0
neg : max p.support.max (↑n : WithBot ℕ) ≤ max p.degree (↑n : WithBot ℕ)
⊢ (insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)

Tactic:
rw [max_insert, max_comm]

Premises used: Finset.max_insert, max_comm
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
h : ¬a = 0
⊢ max p.support.max (↑n : WithBot ℕ) ≤ max p.degree (↑n : WithBot ℕ)

Tactic:
le_rfl

Premises used: le_rfl, Polynomial.degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
h : ¬a = 0
⊢ max p.support.max (↑n : WithBot ℕ) ≤ max p.degree (↑n : WithBot ℕ)

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
rw : (p.update n a).support.max ≤ max p.degree (↑n : WithBot ℕ)
rw₁ rw₂ rw₃ : (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
pos : a = 0 → (p.support.erase n).max ≤ max p.degree (↑n : WithBot ℕ)
neg neg₁ : ¬a = 0 → (insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
⊢ (p.update n a).degree ≤ max p.degree (↑n : WithBot ℕ)

Tactic:
classical
  rw [degree, support_update]
  split_ifs
  · exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)
  · rw [max_insert, max_comm]
    exact le_rfl

Premises used: le_rfl, Finset.max_mono, Polynomial.degree, Finset.max_insert, Polynomial.support_update, LE.le.trans, Finset.erase_subset, max_comm
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s : Finset ι
f : ι → R[X]
⊢ degree.{u} (R := R) (∑ i ∈ ∅, f i) ≤ sup ∅ fun (b : ι) ↦ (f b).degree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s_1 : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : degree.{u} (R := R) (∑ i ∈ s, f i) ≤ s.sup fun (b : ι) ↦ (f b).degree
rw : (f a + ∑ x ∈ s, f x).degree ≤ max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i))
⊢ degree.{u} (R := R) (∑ i ∈ cons a s has, f i) ≤ max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i))

Tactic:
rw [Finset.sum_cons]

Premises used: Finset.sum_cons
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s_1 : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : degree.{u} (R := R) (∑ i ∈ s, f i) ≤ s.sup fun (b : ι) ↦ (f b).degree
⊢ (f a + ∑ x ∈ s, f x).degree ≤ max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i))

Tactic:
degree_add_le _ _

Premises used: Polynomial.degree_add_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s_1 : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : degree.{u} (R := R) (∑ i ∈ s, f i) ≤ s.sup fun (b : ι) ↦ (f b).degree
⊢ (f a + ∑ x ∈ s, f x).degree ≤ max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i))

Tactic:
exact degree_add_le _ _

Premises used: Polynomial.degree_add_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s_1 : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : degree.{u} (R := R) (∑ i ∈ s, f i) ≤ s.sup fun (b : ι) ↦ (f b).degree
rw : max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i)) ≤ max (f a).degree (s.sup fun (b : ι) ↦ (f b).degree)
⊢ max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i)) ≤ (cons a s has).sup fun (b : ι) ↦ (f b).degree

Tactic:
rw [sup_cons]

Premises used: Finset.sup_cons
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s_1 : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : degree.{u} (R := R) (∑ i ∈ s, f i) ≤ s.sup fun (b : ι) ↦ (f b).degree
⊢ max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i)) ≤ max (f a).degree (s.sup fun (b : ι) ↦ (f b).degree)

Tactic:
max_le_max le_rfl ih

Premises used: le_rfl, max_le_max
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s_1 : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : degree.{u} (R := R) (∑ i ∈ s, f i) ≤ s.sup fun (b : ι) ↦ (f b).degree
⊢ max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i)) ≤ max (f a).degree (s.sup fun (b : ι) ↦ (f b).degree)

Tactic:
exact max_le_max le_rfl ih

Premises used: le_rfl, max_le_max
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ ∀ (a b : ℕ), (↑(a + b) : WithBot ℕ) ≤ (↑a : WithBot ℕ) + (↑b : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (p * q).degree ≤ p.degree + q.degree

Tactic:
simpa [degree, ← support_toFinsupp] using AddMonoidAlgebra.sup_support_mul_le (by simp) ..

Premises used: Polynomial.degree, AddMonoidAlgebra.sup_support_mul_le, Polynomial.support_toFinsupp
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a b : WithBot ℕ
hp : p.degree ≤ a
hq : q.degree ≤ b
grw : p.degree + q.degree ≤ a + b
grw₁ : a + q.degree ≤ a + b
grw₂ grw₃ : a + b ≤ a + b
⊢ (p * q).degree ≤ a + b

Tactic:
grw [degree_mul_le, hp, hq]

Premises used: Polynomial.degree_mul_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : degree.{u} (R := R) 1 ≤ 0
⊢ (HPow.hPow (β := ℕ) p 0).degree ≤ HSMul.hSMul (α := ℕ) 0 p.degree

Tactic:
rw [pow_zero, zero_nsmul]

Premises used: pow_zero, zero_nsmul
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ degree.{u} (R := R) 1 ≤ 0

Tactic:
degree_one_le

Premises used: Polynomial.degree_one_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ degree.{u} (R := R) 1 ≤ 0

Tactic:
exact degree_one_le

Premises used: Polynomial.degree_one_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
grw : (p ^ n * p).degree ≤ (n + 1) • p.degree
grw₁ : (p ^ n * p).degree ≤ n • p.degree + p.degree
grw₂ : (p ^ n).degree + p.degree ≤ n • p.degree + p.degree
grw₃ grw₄ : n • p.degree + p.degree ≤ n • p.degree + p.degree
⊢ (p ^ (n + 1)).degree ≤ (n + 1) • p.degree

Tactic:
grw [pow_succ, succ_nsmul, degree_mul_le, degree_pow_le]

Premises used: Polynomial.degree_mul_le, pow_succ, succ_nsmul
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
⊢ (HPow.hPow (β := ℕ) p 0).degree ≤ (↑0 : WithBot ℕ) * a

Tactic:
simp [degree_one_le]

Premises used: Polynomial.degree_one_le
-- 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
succ : (p ^ n * p).degree ≤ (↑n : WithBot ℕ) * a + a
⊢ (p ^ (n + 1)).degree ≤ (↑(n + 1) : WithBot ℕ) * a

Tactic:
rw [Nat.cast_succ, add_mul, one_mul, pow_succ]

Premises used: add_mul, Nat.cast_succ, pow_succ, one_mul
-- 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:
degree_mul_le_of_le hn hp

Premises used: Polynomial.degree_mul_le_of_le