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) (1 : SignType)
h₁ : P.nextCoeff ≠ 0
⊢ P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations

Tactic:
specialize ih _ h_ih (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₁) rfl

Premises used: mt, Polynomial.nextCoeff_eq_zero_of_eraseLead_eq_zero, 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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
simp : Eq (α := ℕ) 0 0
⊢ P.signVariations = P.eraseLead.signVariations + 0

Tactic:
simp [signVariations_eq_eraseLead_add_ite hP, leadingCoeff_eraseLead_eq_nextCoeff h₁,
        hs_nC, h_lC]

Premises used: Polynomial.leadingCoeff_eraseLead_eq_nextCoeff, Polynomial.signVariations_eq_eraseLead_add_ite
-- 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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl

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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
⊢ Eq (α := ℕ) 0 0

Tactic:
exact rfl

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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
⊢ P.signVariations = P.eraseLead.signVariations + 0

Tactic:
have : P.signVariations = P.eraseLead.signVariations + ?_ := by
      simp [signVariations_eq_eraseLead_add_ite hP, leadingCoeff_eraseLead_eq_nextCoeff h₁,
        hs_nC, h_lC]
      exact 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
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]
-- 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)
h₁ : P.nextCoeff ≠ 0
⊢ P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations

Tactic:
specialize ih _ h_ih (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₁) rfl

Premises used: mt, Polynomial.nextCoeff_eq_zero_of_eraseLead_eq_zero, 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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
simp : Eq (α := ℕ) 1 1
⊢ P.signVariations = P.eraseLead.signVariations + 1

Tactic:
simp [signVariations_eq_eraseLead_add_ite hP, leadingCoeff_eraseLead_eq_nextCoeff h₁,
        hs_nC, h_lC]

Premises used: Polynomial.leadingCoeff_eraseLead_eq_nextCoeff, Polynomial.signVariations_eq_eraseLead_add_ite
-- 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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
⊢ Eq (α := ℕ) 1 1

Tactic:
rfl

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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
⊢ Eq (α := ℕ) 1 1

Tactic:
exact rfl

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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
⊢ P.signVariations = P.eraseLead.signVariations + 1

Tactic:
have : P.signVariations = P.eraseLead.signVariations + ?_ := by
      simp [signVariations_eq_eraseLead_add_ite hP, leadingCoeff_eraseLead_eq_nextCoeff h₁,
        hs_nC, h_lC]
      exact 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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
this : P.signVariations = P.eraseLead.signVariations + 0
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
grind [sign_eq_one_iff, signVariations_X_sub_C_mul_eraseLead_le]

Premises used: Polynomial.signVariations_X_sub_C_mul_eraseLead_le, sign_eq_one_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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
this : P.signVariations = P.eraseLead.signVariations + 1
trans :
  P.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations + 1
trans₁ :
  (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
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations

Tactic:
trans ((X - C η) * P).eraseLead.signVariations + 1
-- 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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
this : P.signVariations = P.eraseLead.signVariations + 1
⊢ P.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).eraseLead.signVariations + 1

Tactic:
grind [signVariations_eraseLead_mul_X_sub_C, sign_eq_neg_one_iff]

Premises used: Polynomial.signVariations_eraseLead_mul_X_sub_C, sign_eq_neg_one_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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
this_1 : P.signVariations = P.eraseLead.signVariations + 1
this :
  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)
⊢ (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 +decide [signVariations_eq_eraseLead_add_ite h_mul, h_lC,
          leadingCoeff_eraseLead_eq_nextCoeff, ← sign_eq_zero_iff, this]

Premises used: sign_eq_zero_iff, Polynomial.leadingCoeff_eraseLead_eq_nextCoeff, Polynomial.signVariations_eq_eraseLead_add_ite, Decidable.decide
-- 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 : ℕ
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)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
this : P.signVariations = P.eraseLead.signVariations + 1
suffices :
  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)
⊢ (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:
suffices SignType.sign ((X - C η) * P).nextCoeff = -1 by
        simp +decide [signVariations_eq_eraseLead_add_ite h_mul, h_lC,
          leadingCoeff_eraseLead_eq_nextCoeff, ← sign_eq_zero_iff, this]