awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    EuclideanDomain.r p q
have neg : ∀ (hp : p = 0) (hq : ¬q = 0), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔ p.degree < q.degree
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 _ _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    EuclideanDomain.r p q
have pos₁ : ∀ (hp : ¬p = 0) (hq : q = 0), HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < 0 ↔ p.degree < q.degree
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 _ _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    EuclideanDomain.r p q
have 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
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 _ _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ p.degree = (↑p.natDegree : WithBot ℕ)
have let : ∀ (n : ℕ) (hn : ¬n ∉ p.degree), 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))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬n ∉ p.degree
⊢ p.degree = (↑p.natDegree : WithBot ℕ)
have hn₁ : p.degree = some n
Tactic: have hn : degree p = some n := Classical.not_not.1 hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn_1 : ¬n ∉ p.degree
hn : p.degree = some n
⊢ p.degree = (↑p.natDegree : WithBot ℕ)
have rw : some n = (↑(WithBot.unbotD 0 (some n)) : WithBot ℕ)
Tactic: rw [natDegree, hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.degree = (↑n : WithBot ℕ) ↔ p.natDegree = n
have rw : Eq (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑n : WithBot ℕ) ↔ p.natDegree = n
Tactic: rw [degree_eq_natDegree hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
⊢ p.degree = (↑n : WithBot ℕ) ↔ p.natDegree = n
have inl : degree.{u} (R := R) 0 = (↑n : WithBot ℕ) ↔ natDegree.{u} (R := R) 0 = n
Tactic: obtain rfl | h := eq_or_ne p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ p.degree = (↑n : WithBot ℕ) ↔ p.natDegree = n
have inr : ∀ (h : p ≠ 0), p.degree = (↑n : WithBot ℕ) ↔ p.natDegree = n
Tactic: obtain rfl | h := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.degree = (↑n : WithBot ℕ)
⊢ p.natDegree = n
have rw : WithBot.unbotD 0 p.degree = n
Tactic: rw [natDegree, h, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.degree = (↑n : WithBot ℕ)
rw : WithBot.unbotD 0 p.degree = n
⊢ p.natDegree = n
have rw₁ : WithBot.unbotD 0 (↑n : WithBot ℕ) = n
Tactic: rw [natDegree, h, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ p.natDegree = n
have rw₂ : WithBot.unbotD 0 (↑n : WithBot ℕ) = n
Tactic: rw [natDegree, h, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ p.natDegree = n
have rw₃ : n = n
Tactic: rw [natDegree, h, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree
have rw : WithBot.unbotD 0 q.degree = WithBot.unbotD 0 q.degree
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ (↑n : WithBot ℕ) ≤ p.degree
have rw : (↑n : WithBot ℕ) ≤ p.degree
Tactic: rw [Nat.cast_withBot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
⊢ p.degree ≤ q.degree
have pos : ∀ (hp : p = 0), p.degree ≤ q.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ p.degree ≤ q.degree
have neg : ∀ (hp : ¬p = 0), p.degree ≤ q.degree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
⊢ p.degree ≤ q.degree
have pos : ⊥ ≤ q.degree
Tactic: rw [hp, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ p.degree ≤ q.degree
have neg : (↑p.natDegree : WithBot ℕ) ≤ q.degree
Tactic: rw [degree_eq_natDegree hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : a ≠ 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have rw : (support.{u} (R := R) ((C : (a : R) → R[X]) a)).max = 0
Tactic: rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton,
    WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have rw₁ : (support.{u} (R := R) ((monomial 0 : (a : R) → R[X]) a)).max = 0
Tactic: rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton,
    WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have rw₂ : Eq (α := WithBot ℕ) (Finset.max {0}) 0
Tactic: rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton,
    WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have rw₃ : Eq (α := WithBot ℕ) (sup {0} WithBot.some) 0
Tactic: rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton,
    WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have rw₄ : Eq (α := WithBot ℕ) (↑0 : WithBot ℕ) 0
Tactic: rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton,
    WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have rw₅ : Eq (α := WithBot ℕ) 0 0
Tactic: rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton,
    WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) ≤ 0
have pos : ∀ (h : a = 0), degree.{u} (R := R) ((C : (a : R) → R[X]) a) ≤ 0
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
pos : ∀ (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
have neg : ∀ (h : ¬a = 0), degree.{u} (R := R) ((C : (a : R) → R[X]) a) ≤ 0
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
h : a = 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) ≤ 0
have pos : degree.{u} (R := R) 0 ≤ 0
Tactic: rw [h, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
h : ¬a = 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) ≤ 0
have neg : LE.le (α := WithBot ℕ) 0 0
Tactic: rw [degree_C h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have pos : ∀ (ha : a = 0), natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
pos : ∀ (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
have neg : ∀ (ha : ¬a = 0), natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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])
have rw : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) 0
Tactic: rw [ha, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])
have rw₁ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [ha, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (hypothesis)
Goal:
R : Type u
inst : Semiring R
a : R
ha : a = 0
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have this : Eq (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])
Tactic: have : C a = 0 := by rw [ha, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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])
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have pos : WithBot.unbotD 0 (degree.{u} (R := R) ((C : (a : R) → R[X]) a)) = 0
Tactic: rw [natDegree, degree_eq_bot.2 this, WithBot.unbotD_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have pos₁ : Eq (α := ℕ) (WithBot.unbotD 0 ⊥) 0
Tactic: rw [natDegree, degree_eq_bot.2 this, WithBot.unbotD_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have pos₂ : Eq (α := ℕ) 0 0
Tactic: rw [natDegree, degree_eq_bot.2 this, WithBot.unbotD_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
ha : ¬a = 0
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have neg : WithBot.unbotD 0 (degree.{u} (R := R) ((C : (a : R) → R[X]) a)) = 0
Tactic: rw [natDegree, degree_C ha, WithBot.unbotD_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have neg₁ : Eq (α := ℕ) (WithBot.unbotD 0 0) 0
Tactic: rw [natDegree, degree_C ha, WithBot.unbotD_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0
have neg₂ : Eq (α := ℕ) 0 0
Tactic: rw [natDegree, degree_C ha, WithBot.unbotD_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
ha : a ≠ 0
⊢ degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : WithBot ℕ)
have rw : (support.{u} (R := R) ((monomial n : (a : R) → R[X]) a)).max = (↑n : WithBot ℕ)
Tactic: rw [degree, support_monomial n ha, max_singleton, Nat.cast_withBot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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 ℕ)
⊢ degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : WithBot ℕ)
have rw₁ : Eq (α := WithBot ℕ) (Finset.max {n}) (↑n : WithBot ℕ)
Tactic: rw [degree, support_monomial n ha, max_singleton, Nat.cast_withBot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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 ℕ)
⊢ degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : WithBot ℕ)
have rw₂ : (↑n : WithBot ℕ) = (↑n : WithBot ℕ)
Tactic: rw [degree, support_monomial n ha, max_singleton, Nat.cast_withBot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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 ℕ)
⊢ degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : WithBot ℕ)
have rw₃ : (↑n : WithBot ℕ) = (↑n : WithBot ℕ)
Tactic: rw [degree, support_monomial n ha, max_singleton, Nat.cast_withBot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
ha : a ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).degree = (↑n : WithBot ℕ)
have rw : degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : WithBot ℕ)
Tactic: rw [C_mul_X_pow_eq_monomial, degree_monomial n ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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 ℕ)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).degree = (↑n : WithBot ℕ)
have rw₁ : Eq (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
Tactic: rw [C_mul_X_pow_eq_monomial, degree_monomial n ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) ≤ (↑n : WithBot ℕ)
have rw : LE.le (α := WithBot ℕ) ⊥ (↑n : WithBot ℕ)
Tactic: rw [h, (monomial n).map_zero, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).degree ≤ (↑n : WithBot ℕ)
have rw : degree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) ≤ (↑n : WithBot ℕ)
Tactic: rw [C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : DecidableEq R
i : ℕ
r : R
⊢ natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = if r = 0 then 0 else i
have pos : ∀ (hr : r = 0), natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = 0
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = if r = 0 then 0 else i
have neg : ∀ (hr : ¬r = 0), natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = i
Tactic: split_ifs with hr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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) = i
have neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X i)).natDegree = i
Tactic: rw [← C_mul_X_pow_eq_monomial, natDegree_C_mul_X_pow i r hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ natDegree.{u} (R := R) ((monomial i : (a : R) → R[X]) r) = i
have neg₁ : i = i
Tactic: rw [← C_mul_X_pow_eq_monomial, natDegree_C_mul_X_pow i r hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
⊢ natDegree.{u} (R := R) ((monomial m : (a : R) → R[X]) a) ≤ m
have rw : (if a = 0 then 0 else m) ≤ m
Tactic: rw [Polynomial.natDegree_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
⊢ (if a = 0 then 0 else m) ≤ m
have pos : a = 0 → 0 ≤ m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
pos : a = 0 → 0 ≤ m
⊢ (if a = 0 then 0 else m) ≤ m
have neg : ¬a = 0 → m ≤ m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
⊢ natDegree.{u} (R := R) ((monomial m : (a : R) → R[X]) a) ≤ m
have rw : (if a = 0 then 0 else m) ≤ m
Tactic: classical
  rw [Polynomial.natDegree_monomial]
  split_ifs
  exacts [Nat.zero_le _, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
m : ℕ
rw rw₁ rw₂ : (if a = 0 then 0 else m) ≤ m
⊢ natDegree.{u} (R := R) ((monomial m : (a : R) → R[X]) a) ≤ m
have pos : a = 0 → 0 ≤ m
Tactic: classical
  rw [Polynomial.natDegree_monomial]
  split_ifs
  exacts [Nat.zero_le _, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ natDegree.{u} (R := R) ((monomial m : (a : R) → R[X]) a) ≤ m
have neg : ¬a = 0 → m ≤ m
Tactic: classical
  rw [Polynomial.natDegree_monomial]
  split_ifs
  exacts [Nat.zero_le _, le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.degree.succ = p.natDegree + 1
have rw : WithBot.succ (↑p.natDegree : WithBot ℕ) = p.natDegree + 1
Tactic: rw [degree_eq_natDegree h]