awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
p q : Fq[X]
hp : p = 0
hq : ¬q = 0
⊢ 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔ p.degree < q.degree

Tactic:
simp only [hp, hq, degree_zero, Ne, bot_lt_iff_ne_bot, degree_eq_bot, pow_pos,
          not_false_iff]

Premises used: bot_lt_iff_ne_bot, Ne, Polynomial.degree_zero, not_false_iff, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < 0 ↔ p.degree < q.degree

Tactic:
simp only [hq, degree_zero, not_lt_bot, (pow_pos _).not_gt]

Premises used: not_lt_bot, Polynomial.degree_zero, LT.lt.not_gt
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
neg : LT.lt (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)
⊢ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔
    p.degree < q.degree

Tactic:
rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt, pow_lt_pow_iff_right₀]

Premises used: Polynomial.degree_eq_natDegree, pow_lt_pow_iff_right₀, Nat.cast_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ LT.lt (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)

Tactic:
mod_cast @Fintype.one_lt_card Fq _ _

Premises used: Fintype.one_lt_card, congrArg, Nat.cast_lt._simp_1, cast, Fintype.card, Nat.cast, LT.lt, congrFun', Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ LT.lt (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)

Tactic:
exact mod_cast @Fintype.one_lt_card Fq _ _

Premises used: Fintype.one_lt_card
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
p q : Fq[X]
change :
  LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    p.degree < q.degree
change₁ :
  ((if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) <
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree) ↔
    p.degree < q.degree
pos : ∀ (hp : p = 0) (hq : q = 0), LT.lt (α := ℤ) 0 0 ↔ p.degree < q.degree
neg : ∀ (hp : p = 0) (hq : ¬q = 0), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔ p.degree < q.degree
pos₁ : ∀ (hp : ¬p = 0) (hq : q = 0), HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < 0 ↔ p.degree < q.degree
neg₁ :
  ∀ (hp : ¬p = 0) (hq : ¬q = 0),
    HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔
      p.degree < q.degree
neg₂ : ∀ (hp : p = 0) (hq : ¬q = 0), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔ p.degree < q.degree
pos₂ : ∀ (hp : ¬p = 0) (hq : q = 0), HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < 0 ↔ p.degree < q.degree
neg₃ :
  ∀ (hp : ¬p = 0) (hq : ¬q = 0),
    HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔
      p.degree < q.degree
pos₃ : ∀ (hp : ¬p = 0) (hq : q = 0), HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < 0 ↔ p.degree < q.degree
neg₄ neg₅ :
  ∀ (hp : ¬p = 0) (hq : ¬q = 0),
    HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔
      p.degree < q.degree
⊢ LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    EuclideanDomain.r p q

Tactic:
classical
      change cardPowDegree p < cardPowDegree q ↔ degree p < degree q
      simp only [cardPowDegree_apply]
      split_ifs with hp hq hq
      · simp only [hp, hq, lt_self_iff_false]
      · simp only [hp, hq, degree_zero, Ne, bot_lt_iff_ne_bot, degree_eq_bot, pow_pos,
          not_false_iff]
      · simp only [hq, degree_zero, not_lt_bot, (pow_pos _).not_gt]
      · rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt, pow_lt_pow_iff_right₀]
        exact mod_cast @Fintype.one_lt_card Fq _ _

Premises used: Fintype.one_lt_card, not_lt_bot, bot_lt_iff_ne_bot, Ne, Polynomial.degree, pow_lt_pow_iff_right₀, Polynomial.degree_zero, Polynomial.cardPowDegree_apply, lt_self_iff_false, LT.lt.not_gt, Polynomial.cardPowDegree, not_false_iff, Nat.cast_lt, DFunLike.coe, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.Monic ↔ p.leadingCoeff = 1

Tactic:
Iff.rfl

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

Tactic:
hp

Premises used: Polynomial.Monic
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
⊢ p.coeff p.natDegree = 1

Tactic:
hp

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

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Polynomial.degree, Finset.max, Finset.sup, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
⊢ natDegree.{u} (R := R) 0 = 0

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
⟨fun h => support_eq_empty.1 (Finset.max_eq_bot.1 h), fun h => h.symm ▸ rfl⟩

Premises used: Eq.rec, Finset.max_eq_bot, Iff.intro, Iff.mp, Polynomial.support_eq_empty, Eq.symm, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.degree ≠ ⊥ ↔ p ≠ 0

Tactic:
degree_eq_bot.not

Premises used: Iff.not, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
let : ∀ (n : ℕ) (hn : ¬n ∉ p.degree), p.degree = (↑p.natDegree : WithBot ℕ)
⊢ p.degree = (↑p.natDegree : WithBot ℕ)

Tactic:
let ⟨n, hn⟩ := not_forall.1 (mt Option.eq_none_iff_forall_not_mem.2 (mt degree_eq_bot.1 hp))
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬n ∉ p.degree
⊢ p.degree = some n

Tactic:
have hn : degree p = some n := Classical.not_not.1 hn
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn_1 : ¬n ∉ p.degree
hn : p.degree = some n
rw : some n = (↑(WithBot.unbotD 0 (some n)) : WithBot ℕ)
⊢ p.degree = (↑p.natDegree : WithBot ℕ)

Tactic:
rw [natDegree, hn]

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn_1 : ¬n ∉ p.degree
hn : p.degree = some n
⊢ some n = (↑(WithBot.unbotD 0 (some n)) : WithBot ℕ)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
rw : Eq (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑n : WithBot ℕ) ↔ p.natDegree = n
⊢ p.degree = (↑n : WithBot ℕ) ↔ p.natDegree = n

Tactic:
rw [degree_eq_natDegree hp]

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ Eq (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑n : WithBot ℕ) ↔ p.natDegree = n

Tactic:
WithBot.coe_eq_coe

Premises used: WithBot.coe_eq_coe
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ Eq (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑n : WithBot ℕ) ↔ p.natDegree = n

Tactic:
exact WithBot.coe_eq_coe

Premises used: WithBot.coe_eq_coe
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
inl : degree.{u} (R := R) 0 = (↑n : WithBot ℕ) ↔ natDegree.{u} (R := R) 0 = n
inr : ∀ (h : p ≠ 0), p.degree = (↑n : WithBot ℕ) ↔ p.natDegree = n
⊢ p.degree = (↑n : WithBot ℕ) ↔ p.natDegree = n

Tactic:
obtain rfl | h := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
⊢ degree.{u} (R := R) 0 = (↑n : WithBot ℕ) ↔ natDegree.{u} (R := R) 0 = n

Tactic:
simp [hn.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
h : p ≠ 0
⊢ p.degree = (↑n : WithBot ℕ) ↔ p.natDegree = n

Tactic:
degree_eq_iff_natDegree_eq h

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

Tactic:
exact degree_eq_iff_natDegree_eq h

Premises used: Polynomial.degree_eq_iff_natDegree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.degree = (↑n : WithBot ℕ)
rw : WithBot.unbotD 0 p.degree = n
rw₁ : WithBot.unbotD 0 (↑n : WithBot ℕ) = n
rw₂ : WithBot.unbotD 0 (↑n : WithBot ℕ) = n
rw₃ rw₄ : n = n
⊢ p.natDegree = n

Tactic:
rw [natDegree, h, Nat.cast_withBot, WithBot.unbotD_coe]

Premises used: Nat.cast_withBot, WithBot.unbotD_coe, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ p.natDegree ≠ n → p.degree ≠ (↑n : WithBot ℕ)

Tactic:
mt natDegree_eq_of_degree_eq_some

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

Tactic:
WithBot.giUnbotDBot.gc.le_u_l _

Premises used: GaloisConnection.le_u_l, WithBot.recBotCoe, Polynomial.natDegree, WithBot.giUnbotDBot, WithBot.unbotD, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
q : S[X]
h : p.degree = q.degree
rw rw₁ : WithBot.unbotD 0 q.degree = WithBot.unbotD 0 q.degree
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree

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

Tactic:
rw [Nat.cast_withBot]

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

Tactic:
Finset.le_sup (mem_support_iff.2 h)

Premises used: Iff.mpr, Polynomial.mem_support_iff, Polynomial.degree, Finset.max, Finset.le_sup
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ (↑n : WithBot ℕ) ≤ p.degree

Tactic:
exact Finset.le_sup (mem_support_iff.2 h)

Premises used: Iff.mpr, Polynomial.mem_support_iff, Finset.le_sup
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R[X]
g : S[X]
h : f.support ⊆ g.support
⊢ f.degree ≤ g.degree

Tactic:
Finset.sup_mono h

Premises used: Polynomial.degree, Finset.sup_mono, Finset.max
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
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.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
pos : ⊥ ≤ q.degree
⊢ p.degree ≤ q.degree

Tactic:
rw [hp, degree_zero]

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

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
⊢ ⊥ ≤ q.degree

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
neg : (↑p.natDegree : WithBot ℕ) ≤ q.degree
⊢ p.degree ≤ q.degree

Tactic:
rw [degree_eq_natDegree hp]

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ (↑p.natDegree : WithBot ℕ) ≤ q.degree

Tactic:
le_degree_of_ne_zero h

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

Tactic:
exact le_degree_of_ne_zero h

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

Tactic:
WithBot.unbotD_le_iff (fun _ ↦ bot_le)

Premises used: WithBot.unbotD_le_iff, Polynomial.natDegree, bot_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ p.natDegree < n ↔ p.degree < (↑n : WithBot ℕ)

Tactic:
WithBot.unbotD_lt_iff (absurd · (degree_eq_bot.not.mpr hp))

Premises used: Iff.mpr, WithBot.unbotD_lt_iff, Iff.not, absurd, Polynomial.natDegree, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
q : S[X]
hpq : p.degree ≤ q.degree
⊢ p.natDegree ≤ q.natDegree

Tactic:
WithBot.giUnbotDBot.gc.monotone_l hpq

Premises used: Polynomial.natDegree, GaloisConnection.monotone_l, WithBot.giUnbotDBot, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
a : R
inst : Semiring R
ha : a ≠ 0
rw : (support.{u} (R := R) ((C : (a : R) → R[X]) a)).max = 0
rw₁ : (support.{u} (R := R) ((monomial 0 : (a : R) → R[X]) a)).max = 0
rw₂ : Eq (α := WithBot ℕ) (Finset.max {0}) 0
rw₃ : Eq (α := WithBot ℕ) (sup {0} WithBot.some) 0
rw₄ : Eq (α := WithBot ℕ) (↑0 : WithBot ℕ) 0
rw₅ rw₆ : Eq (α := WithBot ℕ) 0 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0

Tactic:
rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton,
    WithBot.coe_zero]

Premises used: Polynomial.support_monomial, Finset.sup_singleton, Finset.max_eq_sup_coe, Polynomial.degree, Polynomial.monomial_zero_left, OfNat.ofNat, WithBot.coe_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
a : R
inst : Semiring R
pos : ∀ (h : a = 0), degree.{u} (R := R) ((C : (a : R) → R[X]) a) ≤ 0
neg : ∀ (h : ¬a = 0), degree.{u} (R := R) ((C : (a : R) → R[X]) a) ≤ 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) ≤ 0

Tactic:
by_cases h : a = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
a : R
inst : Semiring R
h : a = 0
pos : degree.{u} (R := R) 0 ≤ 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) ≤ 0

Tactic:
rw [h, C_0]

Premises used: Polynomial.C_0
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
a : R
inst : Semiring R
h : a = 0
⊢ degree.{u} (R := R) 0 ≤ 0

Tactic:
bot_le

Premises used: Multiset.foldr, Finset.fold, Polynomial.degree, Finset.max, Finset.sup, List.foldr, bot_le, Multiset.fold
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
a : R
inst : Semiring R
h : a = 0
⊢ degree.{u} (R := R) 0 ≤ 0

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
a : R
inst : Semiring R
h : ¬a = 0
neg neg₁ : LE.le (α := WithBot ℕ) 0 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) ≤ 0

Tactic:
rw [degree_C h]

Premises used: Polynomial.degree_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
a : R
inst : Semiring R
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) < 1

Tactic:
degree_C_le.trans_lt <| WithBot.coe_lt_coe.mpr zero_lt_one

Premises used: Iff.mpr, zero_lt_one, WithBot.coe_lt_coe, LE.le.trans_lt, Polynomial.degree_C_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) 1) ≤ 0

Tactic:
degree_C_le

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

Tactic:
exact degree_C_le

Premises used: Polynomial.degree_C_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
pos : ∀ (ha : a = 0), natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
neg : ∀ (ha : ¬a = 0), natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
ha : a = 0
rw : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) 0
rw₁ rw₂ : Eq.{u + 1} (α := R[X]) 0 0
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])

Tactic:
rw [ha, C_0]

Premises used: Polynomial.C_0
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
ha : a = 0
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])

Tactic:
have : C a = 0 := by rw [ha, C_0]
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
ha : a = 0
this : Eq (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])
pos : WithBot.unbotD 0 (degree.{u} (R := R) ((C : (a : R) → R[X]) a)) = 0
pos₁ : Eq (α := ℕ) (WithBot.unbotD 0 ⊥) 0
pos₂ pos₃ : Eq (α := ℕ) 0 0
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0

Tactic:
rw [natDegree, degree_eq_bot.2 this, WithBot.unbotD_bot]

Premises used: Iff.mpr, WithBot.unbotD_bot, Polynomial.natDegree, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
ha : ¬a = 0
neg : WithBot.unbotD 0 (degree.{u} (R := R) ((C : (a : R) → R[X]) a)) = 0
neg₁ : Eq (α := ℕ) (WithBot.unbotD 0 0) 0
neg₂ neg₃ : Eq (α := ℕ) 0 0
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0

Tactic:
rw [natDegree, degree_C ha, WithBot.unbotD_zero]

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

Tactic:
natDegree_C 1

Premises used: Polynomial.natDegree_C, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ natDegree.{u} (R := R) (↑n : R[X]) = 0

Tactic:
simp only [← C_eq_natCast, natDegree_C]

Premises used: Polynomial.C_eq_natCast, Polynomial.natDegree_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ natDegree.{u} (R := R) (OfNat.ofNat n) = 0

Tactic:
natDegree_natCast _

Premises used: Polynomial.natDegree_natCast
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ natDegree.{u} (R := R) (↑n : R[X]) ≤ Zero.zero

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
ha : a ≠ 0
rw : (support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)).max = (↑n : WithBot ℕ)
rw₁ : Eq (α := WithBot ℕ) (Finset.max {n}) (↑n : WithBot ℕ)
rw₂ : (↑n : WithBot ℕ) = (↑n : WithBot ℕ)
rw₃ rw₄ : (↑n : WithBot ℕ) = (↑n : WithBot ℕ)
⊢ degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : WithBot ℕ)

Tactic:
rw [degree, support_monomial n ha, max_singleton, Nat.cast_withBot]

Premises used: Polynomial.support_monomial, Finset.max_singleton, Polynomial.degree, Nat.cast_withBot
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
ha : a ≠ 0
rw : degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : WithBot ℕ)
rw₁ rw₂ : Eq (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).degree = (↑n : WithBot ℕ)

Tactic:
rw [C_mul_X_pow_eq_monomial, degree_monomial n ha]

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

Tactic:
simpa only [pow_one] using degree_C_mul_X_pow 1 ha

Premises used: pow_one, OfNat.ofNat, Polynomial.degree_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
rw : LE.le (α := WithBot ℕ) ⊥ (↑n : WithBot ℕ)
⊢ degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) ≤ (↑n : WithBot ℕ)

Tactic:
rw [h, (monomial n).map_zero, degree_zero]

Premises used: LinearMap.map_zero, Polynomial.monomial, Polynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ LE.le (α := WithBot ℕ) ⊥ (↑n : WithBot ℕ)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ LE.le (α := WithBot ℕ) ⊥ (↑n : WithBot ℕ)

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
rw : degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) ≤ (↑n : WithBot ℕ)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).degree ≤ (↑n : WithBot ℕ)

Tactic:
rw [C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) ≤ (↑n : WithBot ℕ)

Tactic:
apply degree_monomial_le

Premises used: Polynomial.degree_monomial_le
-- 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).degree ≤ 1

Tactic:
simpa only [pow_one] using degree_C_mul_X_pow_le 1 a

Premises used: Polynomial.degree_C_mul_X_pow_le, pow_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
ha : a ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = n

Tactic:
natDegree_eq_of_degree_eq_some (degree_C_mul_X_pow n ha)

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Defs
Goal:
R : Type u
inst : Semiring R
a : R
ha : a ≠ 0
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree = 1

Tactic:
simpa only [pow_one] using natDegree_C_mul_X_pow 1 a ha

Premises used: Polynomial.natDegree_C_mul_X_pow, pow_one, OfNat.ofNat