awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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 : (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 =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead

Tactic:
rw [he, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
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
⊢ (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
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead = 0

Tactic:
simp [he₂]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
rw : #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.support = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead = 0

Tactic:
rw [← card_support_eq_zero]

Premises used: Polynomial.card_support_eq_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
linarith :
  #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.support < 0 →
    -1 +
          HSub.hSub (α := ℤ) 0
            (↑(#(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.support) :
              ℤ) +
        (HAdd.hAdd (α := ℤ)
            (↑(#(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.support) :
              ℤ)
            1 -
          0) =
      0
linarith₁ :
  0 < #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.support →
    -1 +
              HSub.hSub (α := ℤ)
                (↑(#(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support) : ℤ) 2 +
            (HAdd.hAdd (α := ℤ) 0 1 -
              (↑(#(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) *
                            P).eraseLead.eraseLead.support) :
                ℤ)) +
          (HAdd.hAdd (α := ℤ)
              (↑(#(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) *
                            P).eraseLead.eraseLead.support) :
                ℤ)
              1 -
            (↑(#(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.support) : ℤ)) +
        (HAdd.hAdd (α := ℤ)
            (↑(#(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.support) : ℤ) 1 -
          (↑(#(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support) : ℤ)) =
      0
⊢ #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.support = 0

Tactic:
linarith [eraseLead_support_card_lt he₂,
        eraseLead_support_card_lt (mul_ne_zero (X_sub_C_ne_zero x) hp)]

Premises used: Polynomial.eraseLead_support_card_lt, mul_ne_zero, Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
neg : #(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

Tactic:
suffices #((X - C x) * P).support ≤ 2 by
      rw [← card_support_eq_zero]
      linarith [eraseLead_support_card_lt he₂,
        eraseLead_support_card_lt (mul_ne_zero (X_sub_C_ne_zero x) hp)]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).support = 2

Tactic:
simpa [← sub_eq_add_neg] using
        card_support_binomial one_ne_zero one_ne_zero (neg_ne_zero.mpr hx)

Premises used: Iff.mpr, sub_eq_add_neg, Polynomial.card_support_binomial, neg_ne_zero, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).support = 2

Tactic:
have h₂ : #(X - C x).support = 2 := by
      simpa [← sub_eq_add_neg] using
        card_support_binomial one_ne_zero one_ne_zero (neg_ne_zero.mpr hx)
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₂ : #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).support = 2
⊢ #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support ≤
    #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).support * #P.support

Tactic:
have hmul := card_support_mul_le (p := X - C x) (q := P)
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₂ : #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).support = 2
hmul :
  #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support ≤
    #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).support * #P.support
⊢ #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support ≤ 2 * #P.support

Tactic:
rw [h₂] at hmul
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₂ : #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).support = 2
hmul : #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support ≤ 2 * #P.support
linarith :
  2 < #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support →
    -1 +
            ((↑(#(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support) : ℤ) -
              HMul.hMul (α := ℤ) 2 (↑(#P.support) : ℤ)) +
          (HAdd.hAdd (α := ℤ) 2 1 -
            (↑(#(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support) : ℤ)) +
        2 * HSub.hSub (α := ℤ) (↑(#P.support) : ℤ) 1 =
      0
linarith₁ : 2 < #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support → GT.gt (α := ℤ) 2 0
⊢ #(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).support ≤ 2

Tactic:
linarith [card_support_le_one_of_eraseLead_eq_zero he]

Premises used: Polynomial.card_support_le_one_of_eraseLead_eq_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree + P.natDegree = P.natDegree + 1
rw₁ : 1 + P.natDegree = P.natDegree + 1
rw₂ rw₃ : P.natDegree + 1 = P.natDegree + 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1

Tactic:
rw [natDegree_mul (X_sub_C_ne_zero x) hp, natDegree_X_sub_C, add_comm]

Premises used: Polynomial.natDegree_mul, Polynomial.natDegree_X_sub_C, add_comm, Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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).natDegree = P.natDegree + 1

Tactic:
have h₁ : ((X - C x) * P).natDegree = P.natDegree + 1 := by
    rw [natDegree_mul (X_sub_C_ne_zero x) hp, natDegree_X_sub_C, add_comm]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
neg :
  ∀ (dP : ℕ) (hdP : P.natDegree = dP + 2),
    (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

Tactic:
obtain ⟨dP, hdP⟩ := Nat.exists_eq_add_of_le' (two_le_natDegree_of_nextCoeff_eraseLead he h)

Premises used: Polynomial.two_le_natDegree_of_nextCoeff_eraseLead, Nat.exists_eq_add_of_le'
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
⊢ P.coeff (dP + 1) = 0

Tactic:
simp only [nextCoeff, hdP, Nat.succ_ne_zero, ite_false, Nat.add_one_sub_one] at h

Premises used: Nat.add_one_sub_one, ite_false, Polynomial.nextCoeff, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h : P.coeff (dP + 1) = 0
rw : (if dP + 2 + 1 = 0 then 0 else P.coeff (dP + 1) - x * P.coeff (dP + 1 + 1)) ≠ 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0

Tactic:
rw [nextCoeff, h₁, add_tsub_cancel_right, hdP, coeff_X_sub_C_mul]

Premises used: Polynomial.coeff_X_sub_C_mul, Polynomial.nextCoeff, add_tsub_cancel_right
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h : P.coeff (dP + 1) = 0
⊢ (if dP + 2 + 1 = 0 then 0 else P.coeff (dP + 1) - x * P.coeff (dP + 1 + 1)) ≠ 0

Tactic:
simp [h, hx, ← hdP, hp]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0

Tactic:
have h₂ : ((X - C x) * P).nextCoeff ≠ 0 := by
    simp only [nextCoeff, hdP, Nat.succ_ne_zero, ite_false, Nat.add_one_sub_one] at h
    rw [nextCoeff, h₁, add_tsub_cancel_right, hdP, coeff_X_sub_C_mul]
    simp [h, hx, ← hdP, hp]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
neg :
  ∀ (n : ℕ),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.coeff n =
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n
⊢ (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:
ext n
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
neg :
  ∀ (hn : n < P.natDegree),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.coeff n =
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n
neg₁ :
  ∀ (hn : n ≥ P.natDegree),
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.coeff n =
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.coeff n =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n

Tactic:
rcases n.lt_or_ge P.natDegree with hn | hn

Premises used: Nat.lt_or_ge, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
linarith :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree ≤ n →
    -1 +
              -((↑(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree : ℤ) -
                  HAdd.hAdd (α := ℤ) (↑P.natDegree : ℤ) 1) +
            (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - (↑P.natDegree : ℤ)) +
          HSub.hSub (α := ℤ)
            (↑(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree : ℤ)
            (↑n : ℤ) +
        -(HAdd.hAdd (α := ℤ)
              (↑(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree : ℤ) 1 -
            (↑(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree : ℤ)) =
      0
⊢ n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree

Tactic:
linarith [natDegree_eraseLead_add_one h₂]

Premises used: Polynomial.natDegree_eraseLead_add_one
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
⊢ n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree

Tactic:
have hd₁ : n < ((X - C x) * P).eraseLead.natDegree := by
      linarith [natDegree_eraseLead_add_one h₂]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree
neg :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.coeff n - 0 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.coeff n =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n

Tactic:
rw [← self_sub_monomial_natDegree_leadingCoeff, coeff_sub, coeff_monomial, if_neg hd₁.ne']

Premises used: Polynomial.self_sub_monomial_natDegree_leadingCoeff, Polynomial.coeff_monomial, LT.lt.ne', Polynomial.coeff_sub, if_neg
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree
⊢ ¬(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = n

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree
neg :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).coeff n - 0 - 0 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.coeff n - 0 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n

Tactic:
rw [← self_sub_monomial_natDegree_leadingCoeff, coeff_sub, coeff_monomial, if_neg (by lia)]

Premises used: Polynomial.self_sub_monomial_natDegree_leadingCoeff, Polynomial.coeff_monomial, Polynomial.coeff_sub, if_neg
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree
neg :
  (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
          ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff : R[X])).coeff
      n =
    0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).coeff n - 0 - 0 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n

Tactic:
rw [← self_sub_monomial_natDegree_leadingCoeff, mul_sub, coeff_sub,
      sub_zero, sub_zero, eq_sub_iff_add_eq, add_eq_left]

Premises used: mul_sub, Polynomial.self_sub_monomial_natDegree_leadingCoeff, sub_zero, eq_sub_iff_add_eq, add_eq_left, Polynomial.coeff_sub
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree
neg :
  ∀ (hn₂ : n = 0),
    (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
            ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff : R[X])).coeff
        0 =
      0
neg₁ :
  ∀ (n_1 : ℕ) (hn₂ : n = n_1 + 1),
    (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
            ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff : R[X])).coeff
        (n_1 + 1) =
      0
⊢ (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
          ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff : R[X])).coeff
      n =
    0

Tactic:
rcases hn₂ : n
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree
hn₂ : n = 0
h_1 : P.natDegree = 0
⊢ x = 0

Tactic:
lia