awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
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
ih :
  ∀ m < 0,
    ∀ {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 = 0
hcQ : 0 < P.coeff 0
hxcQ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff 1 = P.coeff 0
⊢ List.length (α := SignType)
          (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
            (List.filter (fun (x : SignType) ↦ decide ¬x = 0)
              (List.map (⇑SignType.sign : (a : R) → SignType) (List.map P.coeff (List.range P.degree.succ).reverse)))) -
        1 +
      1 ≤
    List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
          (List.filter (fun (x : SignType) ↦ decide ¬x = 0)
            (List.map (⇑SignType.sign : (a : R) → SignType)
              (List.map (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff
                (List.range
                    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).degree.succ).reverse)))) -
      1
have zero : List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
          (List.filter (fun (x : SignType) ↦ decide ¬x = 0)
            (List.map (⇑SignType.sign : (a : R) → SignType)
              (List.map P.coeff (List.range (P.natDegree + 1)).reverse)))) -
      1 +
    1 ≤
  List.length (α := SignType)
      (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
        (List.filter (fun (x : SignType) ↦ decide ¬x = 0)
          (List.map (⇑SignType.sign : (a : R) → SignType)
            (List.map (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff
              (List.range
                  ((HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree +
                    1)).reverse)))) -
    1
Tactic: rw [withBotSucc_degree_eq_natDegree_add_one hP, withBotSucc_degree_eq_natDegree_add_one h_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
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
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have succ : ∀ (s_nC : SignType) (hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC),
  P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
Tactic: generalize hs_nC : SignType.sign P.nextCoeff = s_nC
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
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 : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have succ : ∀ (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),
  P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
Tactic: generalize hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
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 : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
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
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have h_ih : P.eraseLead.natDegree < d + 1
Tactic: have h_ih : P.eraseLead.natDegree < d + 1 := by grind [eraseLead_natDegree_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
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 : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
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
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have 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)
Tactic: have h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1 := by simp [h_lC]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
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 : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
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)
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have h_ηP : 0 < η * P.coeff (d + 1)
Tactic: have h_ηP : 0 < η * coeff P (d + 1) := by grind [leadingCoeff, mul_pos]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
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 : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
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)
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have succ : ∀ (hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (-1 : SignType)),
  P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
Tactic: rcases s_nC.trichotomy with rfl | rfl | rfl
Cleared hypotheses: s_nC, hs_nC
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
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 : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
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)
succ :
  ∀ (hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (-1 : SignType)),
    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
have succ₁ : ∀ (hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)),
  P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
Tactic: rcases s_nC.trichotomy with rfl | rfl | rfl
Cleared hypotheses: s_nC, hs_nC
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
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 : SignType
hs_nC : (SignType.sign : (a : R) → SignType) P.nextCoeff = s_nC
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)
succ :
  ∀ (hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (-1 : SignType)),
    P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
succ₁ :
  ∀ (hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (0 : SignType)),
    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
have succ₂ : ∀ (hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (1 : SignType)),
  P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
Tactic: rcases s_nC.trichotomy with rfl | rfl | rfl
Cleared hypotheses: s_nC, hs_nC
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
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)
⊢ s_nC_mul = -1
have this : P.coeff d = 0
Tactic: have : coeff P d = 0 := by simpa [nextCoeff, hd] using hs_nC
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
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.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have 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)
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]
Cleared hypotheses: s_nC_mul, hs_nC_mul
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
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)
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have pos : P.eraseLead = 0 →
  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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
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
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have neg : ¬P.eraseLead = 0 →
  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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
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
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
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
have 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
Tactic: have := signVariations_eraseLead_le (eraseLead ((X - C η) * P))