awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
⊢ P.coeff d = 0

Tactic:
simpa [nextCoeff, hd] using hs_nC

Premises used: Polynomial.nextCoeff
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
⊢ P.coeff d = 0

Tactic:
have : coeff P d = 0 := by simpa [nextCoeff, hd] using hs_nC
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
this : P.coeff d = 0
⊢ s_nC_mul = -1

Tactic:
simp [*, ← hs_nC_mul, nextCoeff, coeff_X_sub_C_mul]

Premises used: Polynomial.coeff_X_sub_C_mul, Polynomial.nextCoeff
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)

Tactic:
obtain rfl : s_nC_mul = -1 := by
      have : coeff P d = 0 := by simpa [nextCoeff, hd] using hs_nC
      simp [*, ← hs_nC_mul, nextCoeff, coeff_X_sub_C_mul]

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
hs_nC_mul :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)
pos :
  P.eraseLead = 0 →
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
neg :
  ¬P.eraseLead = 0 →
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
by_cases eraseLead P = 0

Premises used: Polynomial.eraseLead
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
hs_nC_mul :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)
h : P.eraseLead = 0
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
grind [succ_signVariations_X_sub_C_mul_monomial,
        eraseLead_add_monomial_natDegree_leadingCoeff, zero_add]

Premises used: Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff, zero_add, Polynomial.succ_signVariations_X_sub_C_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
hs_nC_mul :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)
h : ¬P.eraseLead = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations + 1 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
simp [-leadingCoeff_mul, ← sign_ne_zero,
          signVariations_eq_eraseLead_add_ite h_mul, leadingCoeff_eraseLead_eq_nextCoeff,
          hs_nC_mul, h_mul_lC]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.leadingCoeff_eraseLead_eq_nextCoeff, Polynomial.signVariations_eq_eraseLead_add_ite, sign_ne_zero
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
hs_nC_mul :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)
h : ¬P.eraseLead = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations + 1 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
have : signVariations ((X - C η) * P).eraseLead + 1 =
          signVariations ((X - C η) * P) := by
        simp [-leadingCoeff_mul, ← sign_ne_zero,
          signVariations_eq_eraseLead_add_ite h_mul, leadingCoeff_eraseLead_eq_nextCoeff,
          hs_nC_mul, h_mul_lC]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
hs_nC_mul :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)
h : ¬P.eraseLead = 0
this :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations + 1 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.eraseLead.signVariations ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations

Tactic:
have := signVariations_eraseLead_le (eraseLead ((X - C η) * P))
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
hs_nC_mul :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)
h : ¬P.eraseLead = 0
this_1 :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations + 1 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
this :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.eraseLead.signVariations ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations
rwa : P.nextCoeff = 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations

Tactic:
rwa [← eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero hη.ne']

Premises used: LT.lt.ne', Polynomial.eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
hs_nC_mul :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)
h : ¬P.eraseLead = 0
this_1 :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations + 1 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
this :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.eraseLead.signVariations ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations
⊢ P.nextCoeff = 0

Tactic:
grind [sign_eq_zero_iff]

Premises used: sign_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
hs_nC_mul :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)
h : ¬P.eraseLead = 0
this :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations + 1 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations

Tactic:
have : ((X - C η) * P.eraseLead).signVariations ≤
          ((X - C η) * P).eraseLead.signVariations := by
        have := signVariations_eraseLead_le (eraseLead ((X - C η) * P))
        rwa [← eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero hη.ne']
        grind [sign_eq_zero_iff]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)
hs_nC_mul :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)
h : ¬P.eraseLead = 0
this_1 :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations + 1 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
this :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
grind [signVariations_le_eraseLead_succ]

Premises used: Polynomial.signVariations_le_eraseLead_succ
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (1 : SignType)
⊢ P.nextCoeff ≠ 0

Tactic:
simp [← sign_ne_zero, hs_nC]

Premises used: sign_ne_zero
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
ih :
  ∀ m < d + 1,
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = m),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (1 : SignType)
⊢ P.nextCoeff ≠ 0

Tactic:
have h₁ : nextCoeff P ≠ 0 := by simp [← sign_ne_zero, hs_nC]