awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
zero :
  (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.zero →
    SignType.zero = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
    (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
have neg : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.neg →
  SignType.neg = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
Tactic: cases _ : SignType.sign P.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
zero :
  (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.zero →
    SignType.zero = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
neg :
  (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.neg →
    SignType.neg = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
    (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
have pos : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.pos →
  SignType.pos = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
Tactic: cases _ : SignType.sign P.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
h_1 : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.zero
⊢ SignType.zero = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
have zero : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero → SignType.zero = -SignType.zero
Tactic: cases _ : SignType.sign P.eraseLead.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
h_1 : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.zero
zero : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero → SignType.zero = -SignType.zero
⊢ SignType.zero = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
have zero₁ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.neg → SignType.zero = -SignType.neg
Tactic: cases _ : SignType.sign P.eraseLead.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
h_1 : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.zero
zero : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero → SignType.zero = -SignType.zero
zero₁ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.neg → SignType.zero = -SignType.neg
⊢ SignType.zero = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
have zero₂ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.pos → SignType.zero = -SignType.pos
Tactic: cases _ : SignType.sign P.eraseLead.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
h_1 : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.neg
⊢ SignType.neg = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
have neg : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero → SignType.neg = -SignType.zero
Tactic: cases _ : SignType.sign P.eraseLead.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
h_1 : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.neg
neg : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero → SignType.neg = -SignType.zero
⊢ SignType.neg = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
have neg₁ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.neg → SignType.neg = -SignType.neg
Tactic: cases _ : SignType.sign P.eraseLead.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
h_1 : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.neg
neg : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero → SignType.neg = -SignType.zero
neg₁ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.neg → SignType.neg = -SignType.neg
⊢ SignType.neg = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
have neg₂ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.pos → SignType.neg = -SignType.pos
Tactic: cases _ : SignType.sign P.eraseLead.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
h_1 : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.pos
⊢ SignType.pos = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
have pos : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero → SignType.pos = -SignType.zero
Tactic: cases _ : SignType.sign P.eraseLead.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
h_1 : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.pos
pos : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero → SignType.pos = -SignType.zero
⊢ SignType.pos = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
have pos₁ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.neg → SignType.pos = -SignType.neg
Tactic: cases _ : SignType.sign P.eraseLead.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) (0 : SignType)
h₄ :
  ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
      ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
h_1 : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.pos
pos : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero → SignType.pos = -SignType.zero
pos₁ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.neg → SignType.pos = -SignType.neg
⊢ SignType.pos = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
have pos₂ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.pos → SignType.pos = -SignType.pos
Tactic: cases _ : SignType.sign P.eraseLead.leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
⊢ P.eraseLead.signVariations ≤ P.signVariations
have pos : ∀ (hpz : P = 0), P.eraseLead.signVariations ≤ P.signVariations
Tactic: by_cases hpz : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
pos : ∀ (hpz : P = 0), P.eraseLead.signVariations ≤ P.signVariations
⊢ P.eraseLead.signVariations ≤ P.signVariations
have neg : ∀ (hpz : ¬P = 0), P.eraseLead.signVariations ≤ P.signVariations
Tactic: by_cases hpz : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
⊢ P.signVariations ≤ P.eraseLead.signVariations + 1
have pos : ∀ (hpz : P = 0), P.signVariations ≤ P.eraseLead.signVariations + 1
Tactic: by_cases hpz : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
pos : ∀ (hpz : P = 0), P.signVariations ≤ P.eraseLead.signVariations + 1
⊢ P.signVariations ≤ P.eraseLead.signVariations + 1
have neg : ∀ (hpz : ¬P = 0), P.signVariations ≤ P.eraseLead.signVariations + 1
Tactic: by_cases hpz : 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 : IsOrderedRing R
P : R[X]
⊢ (-P).signVariations = P.signVariations
have rw : List.length (α := SignType)
      (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
        (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
          (List.map (α := R) (⇑SignType.sign : (a : R) → SignType) (List.map (fun (x : R) ↦ -x) P.coeffList)))) -
    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) P.coeffList))) -
    1
Tactic: rw [signVariations, signVariations, coeffList_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
P : R[X]
⊢ List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
          (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
            (List.map (α := R) (⇑SignType.sign : (a : R) → SignType) (List.map (fun (x : R) ↦ -x) P.coeffList)))) -
      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) P.coeffList))) -
      1
have simp : List.length (α := SignType)
      (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
        (List.map (Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
          (List.filter
            ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘
              Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
            P.coeffList))) -
    1 =
  List.length (α := SignType)
      (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
        (List.map (⇑SignType.sign : (a : R) → SignType)
          (List.filter ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (⇑SignType.sign : (a : R) → SignType)) P.coeffList))) -
    1
Tactic: simp only [List.map_map, List.filter_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
P : R[X]
⊢ List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
          (List.map (Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
            (List.filter
              ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘
                Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
              P.coeffList))) -
      1 =
    List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign : (a : R) → SignType)
            (List.filter ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (⇑SignType.sign : (a : R) → SignType))
              P.coeffList))) -
      1
have hsc : Eq.{u_1 + 1} (α := R → SignType) (Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
  ((fun (x : SignType) ↦ -x) ∘ (⇑SignType.sign : (a : R) → SignType))
Tactic: have hsc : SignType.sign ∘ (fun (x : R) => -x) = (fun x => -x) ∘ SignType.sign := by
    grind [Left.sign_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
P : R[X]
hsc :
  Eq.{u_1 + 1} (α := R → SignType) (Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
    ((fun (x : SignType) ↦ -x) ∘ (⇑SignType.sign : (a : R) → SignType))
⊢ List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
          (List.map (Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
            (List.filter
              ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘
                Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
              P.coeffList))) -
      1 =
    List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign : (a : R) → SignType)
            (List.filter ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (⇑SignType.sign : (a : R) → SignType))
              P.coeffList))) -
      1
have h_neg_destutter : ∀ (l : List SignType),
  Eq (α := List SignType) (List.map (fun (x : SignType) ↦ -x) (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2) l))
    (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2) (List.map (fun (x : SignType) ↦ -x) l))
Tactic: have h_neg_destutter (l : List SignType) :
      (l.destutter (¬· = ·)).map (- ·) = (l.map (- ·)).destutter (¬· = ·) := by
    grind [List.map_destutter, neg_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
P : R[X]
hsc :
  Eq.{u_1 + 1} (α := R → SignType) (Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
    ((fun (x : SignType) ↦ -x) ∘ (⇑SignType.sign : (a : R) → SignType))
h_neg_destutter :
  ∀ (l : List SignType),
    Eq (α := List SignType) (List.map (fun (x : SignType) ↦ -x) (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2) l))
      (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2) (List.map (fun (x : SignType) ↦ -x) l))
⊢ List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
          (List.map (Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
            (List.filter
              ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘
                Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
              P.coeffList))) -
      1 =
    List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign : (a : R) → SignType)
            (List.filter ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (⇑SignType.sign : (a : R) → SignType))
              P.coeffList))) -
      1
have rw : List.length (α := SignType)
      (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
        (List.map (⇑SignType.sign : (a : R) → SignType)
          (List.filter
            ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (fun (x : SignType) ↦ -x) ∘ (⇑SignType.sign : (a : R) → SignType))
            P.coeffList))) -
    1 =
  List.length (α := SignType)
      (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
        (List.map (⇑SignType.sign : (a : R) → SignType)
          (List.filter ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (⇑SignType.sign : (a : R) → SignType)) P.coeffList))) -
    1
Tactic: rw [hsc, List.comp_map, ← h_neg_destutter, List.length_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
P : R[X]
hsc :
  Eq.{u_1 + 1} (α := R → SignType) (Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
    ((fun (x : SignType) ↦ -x) ∘ (⇑SignType.sign : (a : R) → SignType))
h_neg_destutter :
  ∀ (l : List SignType),
    Eq (α := List SignType) (List.map (fun (x : SignType) ↦ -x) (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2) l))
      (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2) (List.map (fun (x : SignType) ↦ -x) l))
⊢ List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
          (List.map (⇑SignType.sign : (a : R) → SignType)
            (List.filter
              ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘
                (fun (x : SignType) ↦ -x) ∘ (⇑SignType.sign : (a : R) → SignType))
              P.coeffList))) -
      1 =
    List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign : (a : R) → SignType)
            (List.filter ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (⇑SignType.sign : (a : R) → SignType))
              P.coeffList))) -
      1
have e_a : Eq.{u_1 + 1} (α := R → Bool)
  ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (fun (x : SignType) ↦ -x) ∘ (⇑SignType.sign : (a : R) → SignType))
  ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (⇑SignType.sign : (a : R) → SignType))
Tactic: congr 5
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
P : R[X]
hsc :
  Eq.{u_1 + 1} (α := R → SignType) (Function.comp (β := R) (⇑SignType.sign : (a : R) → SignType) fun (x : R) ↦ -x)
    ((fun (x : SignType) ↦ -x) ∘ (⇑SignType.sign : (a : R) → SignType))
h_neg_destutter :
  ∀ (l : List SignType),
    Eq (α := List SignType) (List.map (fun (x : SignType) ↦ -x) (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2) l))
      (List.destutter (fun (x1 x2 : SignType) ↦ ¬x1 = x2) (List.map (fun (x : SignType) ↦ -x) l))
⊢ Eq.{u_1 + 1} (α := R → Bool)
    ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (fun (x : SignType) ↦ -x) ∘ (⇑SignType.sign : (a : R) → SignType))
    ((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (⇑SignType.sign : (a : R) → SignType))
have e_a : ∀ (x : R),
  Eq (α := Bool)
    (((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (fun (x : SignType) ↦ -x) ∘ (⇑SignType.sign : (a : R) → SignType)) x)
    (((fun (x : SignType) ↦ decide (x ≠ 0)) ∘ (⇑SignType.sign : (a : R) → SignType)) x)
Tactic: funext
-- 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
P : R[X]
hx : η ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) η : R[X]) P).signVariations = P.signVariations
have inr : ∀
  (this :
    ∀ {R : Type u_1} [inst : Ring R] [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {η : R} (P : R[X]) (hx : η ≠ 0)
      (hx2 : 0 < η), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) η : R[X]) P).signVariations = P.signVariations)
  (hx2 : η ≤ 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) η : R[X]) P).signVariations = P.signVariations
Tactic: wlog! hx2 : 0 < η