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
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
⊢ List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
          (if
              decide (Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) (0 : SignType)) =
                true then
            (SignType.sign : (a : R) → SignType) c₀ ::
              List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)
          else List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)
have isTrue : decide (Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) (0 : SignType)) = true →
  List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
          ((SignType.sign : (a : R) → SignType) c₀ ::
            List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)
Tactic: split
-- 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
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
isTrue :
  decide (Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) (0 : SignType)) = true →
    List.length (α := SignType)
        (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
          (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
      List.length (α := SignType)
        (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
            ((SignType.sign : (a : R) → SignType) c₀ ::
              List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
          List SignType)
⊢ List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
          (if
              decide (Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) (0 : SignType)) =
                true then
            (SignType.sign : (a : R) → SignType) c₀ ::
              List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)
          else List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)
have isFalse : ¬decide (Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) (0 : SignType)) = true →
  List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)))
Tactic: split
-- 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
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
h_1 : decide (Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) (0 : SignType)) = true
⊢ List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (if Ne (α := SignType) (1 : SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) then
          1 ::
            List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) ((SignType.sign : (a : R) → SignType) c₀)
              (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))
        else
          List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
            (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)
have isTrue : Ne (α := SignType) (1 : SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) →
  List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (1 ::
          List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) ((SignType.sign : (a : R) → SignType) c₀)
            (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)
Tactic: split
-- 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
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
h_1 : decide (Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) (0 : SignType)) = true
isTrue :
  Ne (α := SignType) (1 : SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) →
    List.length (α := SignType)
        (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
          (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
      List.length (α := SignType)
        (1 ::
            List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) ((SignType.sign : (a : R) → SignType) c₀)
              (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
          List SignType)
⊢ List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (if Ne (α := SignType) (1 : SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) then
          1 ::
            List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) ((SignType.sign : (a : R) → SignType) c₀)
              (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))
        else
          List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
            (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)
have isTrue₁ : ¬Ne (α := SignType) (1 : SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) →
  List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)))
Tactic: split
-- 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
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
h_1 : decide (Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) (0 : SignType)) = true
h_2 : Ne (α := SignType) (1 : SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType)
⊢ List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (1 ::
          List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) ((SignType.sign : (a : R) → SignType) c₀)
            (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)
have isTrue : ∀
  (hcs :
    Eq (α := List SignType)
      (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) []),
  List.length (α := SignType) (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1 []) ≤
    List.length (α := SignType)
      (1 :: List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) ((SignType.sign : (a : R) → SignType) c₀) [] :
        List SignType)
Tactic: rcases hcs : (cs.map SignType.sign).filter fun x ↦ decide (x ≠ 0) with _ | ⟨r, rs⟩
-- 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
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList = P.nextCoeff :: cs
h_1 : decide (Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType) (0 : SignType)) = true
h_2 : Ne (α := SignType) (1 : SignType) ((SignType.sign : (a : R) → SignType) c₀ : SignType)
isTrue :
  ∀
    (hcs :
      Eq (α := List SignType)
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) []),
    List.length (α := SignType) (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1 []) ≤
      List.length (α := SignType)
        (1 :: List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) ((SignType.sign : (a : R) → SignType) c₀) [] :
          List SignType)
⊢ List.length (α := SignType)
      (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs))) ≤
    List.length (α := SignType)
      (1 ::
          List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) ((SignType.sign : (a : R) → SignType) c₀)
            (List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)
have isTrue₁ : ∀ (r : SignType) (rs : List SignType)
  (hcs :
    List.filter (fun (x : SignType) ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs) = r :: rs),
  (List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) 1 (r :: rs)).length ≤
    List.length (α := SignType)
      (1 :: List.destutter' (fun (x1 x2 : SignType) ↦ x1 ≠ x2) ((SignType.sign : (a : R) → SignType) c₀) (r :: rs) :
        List SignType)
Tactic: rcases hcs : (cs.map SignType.sign).filter fun x ↦ decide (x ≠ 0) with _ | ⟨r, rs⟩
-- 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
P : R[X]
η : R
hη : 0 < η
hP : P ≠ 0
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have generalize : ∀ (d : ℕ) (hd : P.natDegree = d),
  P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
Tactic: generalize hd : P.natDegree = d
-- 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 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {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
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have h : ∀
  (H :
    ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = d) (h_lC : 0 < P.leadingCoeff),
      P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations)
  (h_lC : ¬0 < P.leadingCoeff),
  P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
Tactic: wlog h_lC : 0 < leadingCoeff P generalizing P with H
-- 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 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {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
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h :
  ∀
    (H :
      ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = d) (h_lC : 0 < P.leadingCoeff),
        P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations)
    (h_lC : ¬0 < P.leadingCoeff),
    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 wlog : ∀ {P : R[X]} (hP : P ≠ 0) (hd : P.natDegree = d) (h_lC : 0 < P.leadingCoeff),
  P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
Tactic: wlog h_lC : 0 < leadingCoeff P generalizing P with H
Cleared hypotheses: P, hP, hd
-- 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 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {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
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
Tactic: have h_mul : (X - C η) * P ≠ 0 := mul_ne_zero (X_sub_C_ne_zero η) hP
-- 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 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {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
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
have rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).natDegree + P.natDegree = P.natDegree + 1
Tactic: rw [natDegree_mul (X_sub_C_ne_zero η) hP, natDegree_X_sub_C, add_comm]
-- 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 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {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
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).natDegree + P.natDegree = P.natDegree + 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
have rw₁ : 1 + P.natDegree = P.natDegree + 1
Tactic: rw [natDegree_mul (X_sub_C_ne_zero η) hP, natDegree_X_sub_C, add_comm]
-- 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 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {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
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).natDegree + P.natDegree = P.natDegree + 1
rw₁ : 1 + P.natDegree = P.natDegree + 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
have rw₂ : P.natDegree + 1 = P.natDegree + 1
Tactic: rw [natDegree_mul (X_sub_C_ne_zero η) hP, natDegree_X_sub_C, add_comm]
-- 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 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {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
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
Tactic: have h_deg_mul : natDegree ((X - C η) * P) = natDegree P + 1 := by
    rw [natDegree_mul (X_sub_C_ne_zero η) hP, natDegree_X_sub_C, add_comm]
-- 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 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {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
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
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
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have zero : ∀
  (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),
  P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
Tactic: rcases d with _ | d
Cleared hypotheses: d, ih, hd
-- 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 < η
d : ℕ
ih :
  ∀ m < d,
    ∀ {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
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
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
zero :
  ∀
    (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),
    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 : ∀ (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
Tactic: rcases d with _ | d
Cleared hypotheses: d, ih, hd
-- 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
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
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have hcQ : 0 < P.coeff 0
Tactic: have hcQ : 0 < coeff P 0 := by grind [leadingCoeff]
-- 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
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
⊢ P.signVariations + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).signVariations
have hxcQ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeff 1 = P.coeff 0
Tactic: have hxcQ : coeff ((X - C η) * P) 1 = coeff P 0 := by
      simp_all [coeff_X_sub_C_mul, coeff_eq_zero_of_natDegree_lt]