awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
| (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree
have rw : (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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree
have conv : (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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
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
⊢ (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree
have conv₁ : (erase q.natDegree p + -erase q.natDegree 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree
have rw : Eq (α := WithBot ℕ) (↑(p * q).natDegree : WithBot ℕ) (↑(p.natDegree + q.natDegree) : WithBot ℕ)
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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 ℕ)
⊢ (p * q).natDegree = p.natDegree + q.natDegree
have rw₁ : (p * q).degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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 ℕ)
⊢ (p * q).natDegree = p.natDegree + q.natDegree
have rw₂ : (p * q).degree = HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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 ℕ)
⊢ (p * q).natDegree = p.natDegree + q.natDegree
have rw₃ : (p * q).degree = p.degree + (↑q.natDegree : WithBot ℕ)
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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 ℕ)
⊢ (p * q).natDegree = p.natDegree + q.natDegree
have rw₄ : (p * q).degree = p.degree + q.degree
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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
⊢ (p * q).natDegree = p.natDegree + q.natDegree
have rw₅ : p.degree + q.degree = p.degree + q.degree
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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
⊢ (a • p).natDegree = p.natDegree
have pos : ∀ (hp : p = 0), (a • p).natDegree = p.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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
⊢ (a • p).natDegree = p.natDegree
have neg : ∀ (hp : ¬p = 0), (a • p).natDegree = p.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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
have neg : (a • p).natDegree ≤ p.natDegree
Tactic: apply natDegree_eq_of_le_of_coeff_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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
⊢ (a • p).natDegree = p.natDegree
have neg₁ : (a • p).coeff p.natDegree ≠ 0
Tactic: apply natDegree_eq_of_le_of_coeff_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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).coeff p.natDegree ≠ 0
have neg : a • p.coeff p.natDegree ≠ 0
Tactic: simp only [coeff_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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.coeff p.natDegree ≠ 0
have neg : p.coeff p.natDegree ≠ 0
Tactic: apply smul_ne_zero ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
n : ℕ
⊢ (p ^ n).natDegree = n * p.natDegree
have inl : (HPow.hPow (α := R[X]) 0 n).natDegree = n * natDegree.{u} (R := R) 0
Tactic: obtain rfl | hp := eq_or_ne p 0
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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
⊢ (p ^ n).natDegree = n * p.natDegree
have inr : ∀ (hp : p ≠ 0), (p ^ n).natDegree = n * p.natDegree
Tactic: obtain rfl | hp := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
n : ℕ
⊢ (HPow.hPow (α := R[X]) 0 n).natDegree = n * natDegree.{u} (R := R) 0
have inl : (HPow.hPow (α := R[X]) (β := ℕ) 0 0).natDegree = 0 * natDegree.{u} (R := R) 0
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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
⊢ (HPow.hPow (α := R[X]) 0 n).natDegree = n * natDegree.{u} (R := R) 0
have inl₁ : ∀ (hn : n ≠ 0), (HPow.hPow (α := R[X]) 0 n).natDegree = n * natDegree.{u} (R := R) 0
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.leadingCoeff ^ n ≠ 0
have rw : ¬p ^ n = 0
Tactic: rw [← leadingCoeff_pow, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
n : ℕ
⊢ (p ^ n).natDegree = n * p.natDegree
have inl : (HPow.hPow (α := R[X]) 0 n).natDegree = n * natDegree.{u} (R := R) 0
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
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
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
⊢ (p ^ n).natDegree = n * p.natDegree
have inr : ∀ (hp : p ≠ 0), (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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h1 : p ∣ q
h2 : q ≠ 0
⊢ p.natDegree ≤ q.natDegree
have obtain : ∀ (q : R[X]) (h2 : p * q ≠ 0), p.natDegree ≤ (p * q).natDegree
Tactic: obtain ⟨q, rfl⟩ := h1
Cleared hypotheses: q, h1, h2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p.natDegree ≤ (p * q).natDegree
have h2₁ : p ≠ 0 ∧ q ≠ 0
Tactic: rw [mul_ne_zero_iff] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ (p * q).natDegree
have rw : p.natDegree ≤ p.natDegree + q.natDegree
Tactic: rw [natDegree_mul h2.1 h2.2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h1 : p ∣ q
h2 : q ≠ 0
⊢ p.degree ≤ q.degree
have rcases : ∀ (q : R[X]) (h2 : p * q ≠ 0), p.degree ≤ (p * q).degree
Tactic: rcases h1 with ⟨q, rfl⟩
Cleared hypotheses: q, h1, h2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p.degree ≤ (p * q).degree
have h2₁ : p ≠ 0 ∧ q ≠ 0
Tactic: rw [mul_ne_zero_iff] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.degree < p.degree
⊢ q = 0
have by_contra : ∀ (hc : ¬q = 0), False
Tactic: by_contra hc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
⊢ q = 0
have by_contra : ∀ (hc : ¬q = 0), False
Tactic: by_contra hc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ HSub.hSub (α := ℤ) (↑p₁.natDegree : ℤ) (↑q₁.natDegree : ℤ) =
    HSub.hSub (α := ℤ) (↑p₂.natDegree : ℤ) (↑q₂.natDegree : ℤ)
have rw : HAdd.hAdd (α := ℤ) (↑p₁.natDegree : ℤ) (↑q₂.natDegree : ℤ) = HAdd.hAdd (α := ℤ) (↑p₂.natDegree : ℤ) (↑q₁.natDegree : ℤ)
Tactic: rw [sub_eq_sub_iff_add_eq_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ HAdd.hAdd (α := ℤ) (↑p₁.natDegree : ℤ) (↑q₂.natDegree : ℤ) =
    HAdd.hAdd (α := ℤ) (↑p₂.natDegree : ℤ) (↑q₁.natDegree : ℤ)
have norm_cast : p₁.natDegree + q₂.natDegree = p₂.natDegree + q₁.natDegree
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ p₁.natDegree + q₂.natDegree = p₂.natDegree + q₁.natDegree
have rw : (p₁ * q₂).natDegree = p₂.natDegree + q₁.natDegree
Tactic: rw [← natDegree_mul hp₁ hq₂, ← natDegree_mul hp₂ hq₁, h_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
rw : (p₁ * q₂).natDegree = p₂.natDegree + q₁.natDegree
⊢ p₁.natDegree + q₂.natDegree = p₂.natDegree + q₁.natDegree
have rw₁ : (p₁ * q₂).natDegree = (p₂ * q₁).natDegree
Tactic: rw [← natDegree_mul hp₁ hq₂, ← natDegree_mul hp₂ hq₁, h_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Domain (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
rw : (p₁ * q₂).natDegree = p₂.natDegree + q₁.natDegree
rw₁ : (p₁ * q₂).natDegree = (p₂ * q₁).natDegree
⊢ p₁.natDegree + q₂.natDegree = p₂.natDegree + q₁.natDegree
have rw₂ : (p₂ * q₁).natDegree = (p₂ * q₁).natDegree
Tactic: rw [← natDegree_mul hp₁ hq₂, ← natDegree_mul hp₂ hq₁, h_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.IsMonicOfDegree 0 ↔ p = 1
have simp : p.natDegree = 0 ∧ p.Monic ↔ p = 1
Tactic: simp only [isMonicOfDegree_iff']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.natDegree = 0 ∧ p.Monic ↔ p = 1
have refine : ∀ (H : p = 1), p.natDegree = 0 ∧ p.Monic
Tactic: refine ⟨fun ⟨H₁, H₂⟩ ↦ eq_one_of_monic_natDegree_zero H₂ H₁, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
H : p = 1
⊢ p.natDegree = 0 ∧ p.Monic
have subst : natDegree.{u_1} (R := R) 1 = 0 ∧ Monic.{u_1} (R := R) 1
Tactic: subst H
Cleared hypotheses: p, H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
⊢ p.IsMonicOfDegree n ↔ n = 0
have rw : IsMonicOfDegree.{u_1} (R := R) 1 n ↔ n = 0
Tactic: rw [Subsingleton.eq_one p]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
⊢ IsMonicOfDegree.{u_1} (R := R) 1 n ↔ n = 0
have refine_1 : IsMonicOfDegree.{u_1} (R := R) 1 n → ∀ (H : natDegree.{u_1} (R := R) 1 = n), Monic.{u_1} (R := R) 1 → n = 0
Tactic: refine ⟨fun ⟨H, _⟩ ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
refine_1 : IsMonicOfDegree.{u_1} (R := R) 1 n → ∀ (H : natDegree.{u_1} (R := R) 1 = n), Monic.{u_1} (R := R) 1 → n = 0
⊢ IsMonicOfDegree.{u_1} (R := R) 1 n ↔ n = 0
have refine_2 : ∀ (H : n = 0), IsMonicOfDegree.{u_1} (R := R) 1 n
Tactic: refine ⟨fun ⟨H, _⟩ ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
h : IsMonicOfDegree.{u_1} (R := R) 1 n
H : natDegree.{u_1} (R := R) 1 = n
monic : Monic.{u_1} (R := R) 1
⊢ n = 0
have refine_1 : ∀ (H : 0 = n), Monic.{u_1} (R := R) 1 → n = 0
Tactic: rwa [natDegree_one, eq_comm] at H
Cleared hypotheses: H, monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
h : IsMonicOfDegree.{u_1} (R := R) 1 n
H : natDegree.{u_1} (R := R) 1 = n
monic : Monic.{u_1} (R := R) 1
refine_1 : ∀ (H : 0 = n), Monic.{u_1} (R := R) 1 → n = 0
⊢ n = 0
have refine_1₁ : ∀ (H : n = 0), Monic.{u_1} (R := R) 1 → n = 0
Tactic: rwa [natDegree_one, eq_comm] at H
Cleared hypotheses: H, monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
H : n = 0
⊢ IsMonicOfDegree.{u_1} (R := R) 1 n
have refine_2 : IsMonicOfDegree.{u_1} (R := R) 1 0
Tactic: rw [H, isMonicOfDegree_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
H : n = 0
refine_2 : IsMonicOfDegree.{u_1} (R := R) 1 0
⊢ IsMonicOfDegree.{u_1} (R := R) 1 n
have refine_2₁ : Eq.{u_1 + 1} (α := R[X]) 1 1
Tactic: rw [H, isMonicOfDegree_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
⊢ p.IsMonicOfDegree n ↔ p.natDegree ≤ n ∧ p.coeff n = 1
have simp : p.natDegree = n ∧ p.Monic ↔ p.natDegree ≤ n ∧ p.coeff n = 1
Tactic: simp only [isMonicOfDegree_iff']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
⊢ p.natDegree = n ∧ p.Monic ↔ p.natDegree ≤ n ∧ p.coeff n = 1
have refine_1 : p.natDegree ≤ n ∧ p.coeff n = 1 → ∀ (H₁ : p.natDegree ≤ n) (H₂ : p.coeff n = 1), p.natDegree = n
Tactic: refine ⟨fun ⟨H₁, H₂⟩ ↦ ⟨H₁.le, H₁ ▸ Monic.coeff_natDegree H₂⟩, fun ⟨H₁, H₂⟩ ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
refine_1 : p.natDegree ≤ n ∧ p.coeff n = 1 → ∀ (H₁ : p.natDegree ≤ n) (H₂ : p.coeff n = 1), p.natDegree = n
⊢ p.natDegree = n ∧ p.Monic ↔ p.natDegree ≤ n ∧ p.coeff n = 1
have refine_2 : p.natDegree ≤ n ∧ p.coeff n = 1 → ∀ (H₁ : p.natDegree ≤ n) (H₂ : p.coeff n = 1), p.Monic
Tactic: refine ⟨fun ⟨H₁, H₂⟩ ↦ ⟨H₁.le, H₁ ▸ Monic.coeff_natDegree H₂⟩, fun ⟨H₁, H₂⟩ ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ ∃ (q : R[X]), p = HPow.hPow (α := R[X]) X n + q ∧ q.natDegree < n
have refine_1 : p = HPow.hPow (α := R[X]) X n + p.eraseLead
Tactic: refine ⟨p.eraseLead, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
refine_1 : p = HPow.hPow (α := R[X]) X n + p.eraseLead
⊢ ∃ (q : R[X]), p = HPow.hPow (α := R[X]) X n + q ∧ q.natDegree < n
have refine_2 : p.eraseLead.natDegree < n
Tactic: refine ⟨p.eraseLead, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p = HPow.hPow (α := R[X]) X n + p.eraseLead
have refine_1 : p.eraseLead + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
  HPow.hPow (α := R[X]) X n + p.eraseLead
Tactic: nth_rewrite 1 [← p.eraseLead_add_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
    HPow.hPow (α := R[X]) X n + p.eraseLead
have refine_1 : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) + p.eraseLead =
  HPow.hPow (α := R[X]) X n + p.eraseLead
Tactic: rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
refine_1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      p.eraseLead =
    HPow.hPow (α := R[X]) X n + p.eraseLead
⊢ p.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
    HPow.hPow (α := R[X]) X n + p.eraseLead
have refine_1₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X n) + p.eraseLead =
  HPow.hPow (α := R[X]) X n + p.eraseLead
Tactic: rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
refine_1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      p.eraseLead =
    HPow.hPow (α := R[X]) X n + p.eraseLead
refine_1₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X n) + p.eraseLead =
    HPow.hPow (α := R[X]) X n + p.eraseLead
⊢ p.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
    HPow.hPow (α := R[X]) X n + p.eraseLead
have refine_1₂ : (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n + p.eraseLead = HPow.hPow (α := R[X]) X n + p.eraseLead
Tactic: rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]