awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
hr : ¬r = 0
neg :
  Eq.{u_1 + 1} (α := R[X])
    (erase (natDegree.{u_1} (R := R) ((monomial i : (a : R) → R[X]) r)) ((monomial i : (a : R) → R[X]) r)) 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
have neg₁ : Eq.{u_1 + 1} (α := R[X]) (erase (if r = 0 then 0 else i) ((monomial i : (a : R) → R[X]) r)) 0
Tactic: rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
hr : ¬r = 0
neg :
  Eq.{u_1 + 1} (α := R[X])
    (erase (natDegree.{u_1} (R := R) ((monomial i : (a : R) → R[X]) r)) ((monomial i : (a : R) → R[X]) r)) 0
neg₁ : Eq.{u_1 + 1} (α := R[X]) (erase (if r = 0 then 0 else i) ((monomial i : (a : R) → R[X]) r)) 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
have neg₂ : Eq.{u_1 + 1} (α := R[X]) (erase i ((monomial i : (a : R) → R[X]) r)) 0
Tactic: rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
hr : ¬r = 0
neg :
  Eq.{u_1 + 1} (α := R[X])
    (erase (natDegree.{u_1} (R := R) ((monomial i : (a : R) → R[X]) r)) ((monomial i : (a : R) → R[X]) r)) 0
neg₁ : Eq.{u_1 + 1} (α := R[X]) (erase (if r = 0 then 0 else i) ((monomial i : (a : R) → R[X]) r)) 0
neg₂ : Eq.{u_1 + 1} (α := R[X]) (erase i ((monomial i : (a : R) → R[X]) r)) 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
have neg₃ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
have pos : ∀ (hr : r = 0), Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
Tactic: classical
  by_cases hr : r = 0
  · subst r
    simp only [monomial_zero_right, eraseLead_zero]
  · rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
i : ℕ
r : R
pos : ∀ (hr : r = 0), Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
⊢ Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
have neg : ∀ (hr : ¬r = 0), Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial i : (a : R) → R[X]) r)) 0
Tactic: classical
  by_cases hr : r = 0
  · subst r
    simp only [monomial_zero_right, eraseLead_zero]
  · rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).eraseLead = 0
have rw : Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial n : (a : R) → R[X]) 1)) 0
Tactic: rw [X_pow_eq_monomial, eraseLead_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
rw : Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial n : (a : R) → R[X]) 1)) 0
⊢ (HPow.hPow (α := R[X]) X n).eraseLead = 0
have rw₁ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [X_pow_eq_monomial, eraseLead_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).eraseLead = 0
have rw : Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial n : (a : R) → R[X]) r)) 0
Tactic: rw [C_mul_X_pow_eq_monomial, eraseLead_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
rw : Eq.{u_1 + 1} (α := R[X]) (eraseLead ((monomial n : (a : R) → R[X]) r)) 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)).eraseLead = 0
have rw₁ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [C_mul_X_pow_eq_monomial, eraseLead_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
⊢ (p + q).eraseLead = p.eraseLead + q
have a : ∀ (n : ℕ), (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
have pos : ∀ (nd : n = p.natDegree), (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
Tactic: by_cases nd : n = p.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
pos : ∀ (nd : n = p.natDegree), (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
have neg : ∀ (nd : ¬n = p.natDegree), (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
Tactic: by_cases nd : n = p.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : n = p.natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
have pos : 0 = (p.eraseLead + q).coeff p.natDegree
Tactic: rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_left_of_degree_lt pq).symm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (p + q).eraseLead.coeff n = (p.eraseLead + q).coeff n
have neg : ¬n = (p + q).natDegree
Tactic: rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
⊢ (p + q).eraseLead = p + q.eraseLead
have a : ∀ (n : ℕ), (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
have pos : ∀ (nd : n = q.natDegree), (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
Tactic: by_cases nd : n = q.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
pos : ∀ (nd : n = q.natDegree), (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
have neg : ∀ (nd : ¬n = q.natDegree), (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
Tactic: by_cases nd : n = q.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
have pos : 0 = (p + q.eraseLead).coeff q.natDegree
Tactic: rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_right_of_degree_lt pq).symm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n
have neg : ¬n = (p + q).natDegree
Tactic: rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
⊢ 0 < f.natDegree
have by_contra : ∀ (h₂ : ¬0 < f.natDegree), False
Tactic: by_contra h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False
have h₁ : Ne.{u_1 + 1} (α := R[X]) (eraseLead ((C : (a : R) → R[X]) (f.coeff 0))) 0
Tactic: rw [eq_C_of_natDegree_eq_zero (Nat.eq_zero_of_not_pos h₂)] at h
Cleared hypotheses: h, h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
have pos : ∀ (h : #f.support ≤ 1), f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
Tactic: by_cases! h : #f.support ≤ 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
pos : ∀ (h : #f.support ≤ 1), f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
have neg : ∀ (h : 1 < #f.support), f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
Tactic: by_cases! h : #f.support ≤ 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
have pos : f.eraseLead = 0
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead = 0
have pos : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).eraseLead = 0
Tactic: rw [← C_mul_X_pow_eq_self h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : 1 < #f.support
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0
have neg : f.eraseLead.natDegree < f.natDegree
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1
have inl : ∀ (h : f.eraseLead.natDegree < f.natDegree), f.eraseLead.natDegree ≤ f.natDegree - 1
Tactic: rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with (h | h)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
inl : ∀ (h : f.eraseLead.natDegree < f.natDegree), f.eraseLead.natDegree ≤ f.natDegree - 1
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1
have inr : ∀ (h : f.eraseLead = 0), f.eraseLead.natDegree ≤ f.natDegree - 1
Tactic: rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with (h | h)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.natDegree = f.natDegree - 1
have this : 0 < f.natDegree
Tactic: have := natDegree_pos_of_nextCoeff_ne_zero h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.natDegree = f.natDegree - 1
have refine : f.eraseLead.coeff (f.natDegree - 1) ≠ 0
Tactic: refine f.eraseLead_natDegree_le.antisymm <| le_natDegree_of_ne_zero ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this rwa : 0 < f.natDegree
rwa₁ : 0 < f.natDegree
⊢ f.eraseLead.coeff (f.natDegree - 1) ≠ 0
have rwa₂ : LT.lt (α := ℕ) 0 1
Tactic: rwa [eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne, ← nextCoeff_of_natDegree_pos]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.natDegree + 1 = f.natDegree
have rw : 1 ≤ f.natDegree
Tactic: rw [natDegree_eraseLead h, tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff = 0
⊢ f.eraseLead.natDegree ≤ f.natDegree - 2
have refine : f.eraseLead.coeff (f.natDegree - 1) = 0
Tactic: refine natDegree_le_pred (n := f.natDegree - 1) (eraseLead_natDegree_le f) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0
have h₁ : (∃ (x : R), (C : (a : R) → R[X]) x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0
Tactic: rw [nextCoeff_eq_zero, natDegree_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : (∃ (x : R), (C : (a : R) → R[X]) x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0
have inl : ∀ (a : R),
  Eq.{u_1 + 1} (α := R)
    (coeff (eraseLead ((C : (a : R) → R[X]) a)) (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) - 1)) 0
Tactic: obtain ⟨a, rfl⟩ | ⟨hf, h⟩ := h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : (∃ (x : R), (C : (a : R) → R[X]) x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0
inl :
  ∀ (a : R),
    Eq.{u_1 + 1} (α := R)
      (coeff (eraseLead ((C : (a : R) → R[X]) a)) (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) - 1)) 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0
have inr : ∀ (hf : 0 < f.natDegree) (h : f.coeff (f.natDegree - 1) = 0), f.eraseLead.coeff (f.natDegree - 1) = 0
Tactic: obtain ⟨a, rfl⟩ | ⟨hf, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0
have inr : f.nextCoeff = 0
Tactic: rw [eraseLead_coeff_of_ne _ (tsub_lt_self hf zero_lt_one).ne, ← nextCoeff_of_natDegree_pos hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hlead : f.eraseLead ≠ 0
hnext : f.nextCoeff = 0
⊢ 2 ≤ f.natDegree
have contrapose! : ∀ (hlead : f.natDegree < 2), f.eraseLead = 0
Tactic: contrapose! hlead
Cleared hypotheses: hlead
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : f.natDegree < 2
⊢ f.eraseLead = 0
have hlead₁ : (∃ (x : R), (C : (a : R) → R[X]) x = f) ∨
  ∃ (a : R),
    a ≠ 0 ∧
      ∃ (b : R),
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) b : R[X]) =
          f
Tactic: rw [Nat.lt_succ_iff, Nat.le_one_iff_eq_zero_or_eq_one, natDegree_eq_zero, natDegree_eq_one]
    at hlead
Cleared hypotheses: hlead
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead :
  (∃ (x : R), (C : (a : R) → R[X]) x = f) ∨
    ∃ (a : R),
      a ≠ 0 ∧
        ∃ (b : R),
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
              ((C : (a : R) → R[X]) b : R[X]) =
            f
⊢ f.eraseLead = 0
have inl : ∀ (a : R) (hnext : Eq.{u_1 + 1} (α := R) (nextCoeff ((C : (a : R) → R[X]) a)) 0),
  Eq.{u_1 + 1} (α := R[X]) (eraseLead ((C : (a : R) → R[X]) a)) 0
Tactic: obtain ⟨a, rfl⟩ | ⟨a, ha, b, rfl⟩ := hlead
Cleared hypotheses: f, hnext, hlead
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead :
  (∃ (x : R), (C : (a : R) → R[X]) x = f) ∨
    ∃ (a : R),
      a ≠ 0 ∧
        ∃ (b : R),
          HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
              ((C : (a : R) → R[X]) b : R[X]) =
            f
inl :
  ∀ (a : R) (hnext : Eq.{u_1 + 1} (α := R) (nextCoeff ((C : (a : R) → R[X]) a)) 0),
    Eq.{u_1 + 1} (α := R[X]) (eraseLead ((C : (a : R) → R[X]) a)) 0
⊢ f.eraseLead = 0
have inr : ∀ (a : R) (ha : a ≠ 0) (b : R)
  (hnext :
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])).nextCoeff =
      0),
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).eraseLead =
    0
Tactic: obtain ⟨a, rfl⟩ | ⟨a, ha, b, rfl⟩ := hlead
Cleared hypotheses: f, hnext, hlead
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
a : R
ha : a ≠ 0
b : R
hnext :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).nextCoeff =
    0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).eraseLead =
    0
have hnext₁ : b = 0
Tactic: rw [nextCoeff_C_mul_X_add_C ha] at hnext
Cleared hypotheses: hnext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : b = 0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).eraseLead =
    0
have inr : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X + (C : (a : R) → R[X]) 0).eraseLead = 0
Tactic: subst b
Cleared hypotheses: b, hnext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.leadingCoeff = f.nextCoeff
have this : 0 < f.natDegree
Tactic: have := natDegree_pos_of_nextCoeff_ne_zero h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
rw : 0 < f.natDegree
⊢ f.eraseLead.leadingCoeff = f.nextCoeff
have rw₁ : LT.lt (α := ℕ) 0 1
Tactic: rw [leadingCoeff, nextCoeff, natDegree_eraseLead h, if_neg,
    eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
rw : 0 < f.natDegree
rw₁ : LT.lt (α := ℕ) 0 1
⊢ f.eraseLead.leadingCoeff = f.nextCoeff
have hnc : ¬f.natDegree = 0
Tactic: rw [leadingCoeff, nextCoeff, natDegree_eraseLead h, if_neg,
    eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ f.nextCoeff = 0
have by_contra : ∀ (h₂ : ¬f.nextCoeff = 0), False
Tactic: by_contra h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
have pos : ∀ (hp : P = 0),
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
Tactic: by_cases hp : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
pos :
  ∀ (hp : P = 0),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
have neg : ∀ (hp : ¬P = 0),
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
Tactic: by_cases hp : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
have pos : ∀ (he : P.eraseLead = 0),
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
Tactic: by_cases he : P.eraseLead = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
pos :
  ∀ (he : P.eraseLead = 0),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
have neg : ∀ (he : ¬P.eraseLead = 0),
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
Tactic: by_cases he : P.eraseLead = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead
have pos : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead = 0
Tactic: rw [he, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead = 0
have pos : ∀ (he₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead = 0),
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead = 0
Tactic: by_cases he₂ : ((X - C x) * P).eraseLead = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
pos :
  ∀ (he₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead = 0),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead = 0
have neg : ∀ (he₂ : ¬(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead = 0),
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead = 0
Tactic: by_cases he₂ : ((X - C x) * P).eraseLead = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead = 0
this : #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support ≤ 2
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead = 0
have rw : #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.support = 0
Tactic: rw [← card_support_eq_zero]