awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsDomain A
inst_3 : IsDomain B
f : A →+* B
inst_4 : DecidablePred fun (x : B) ↦ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) f) x
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
p : A[X]
a :
  ∀ (b : B),
    count b
        (Multiset.filter (fun (x : B) ↦ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) f) x)
          (map f p).roots) =
      count b (Multiset.map (⇑f : (a : A) → B) p.roots)
a₁ :
  ∀ (b : B),
    (if Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) f) b then count b (map f p).roots else 0) =
      count b (Multiset.map (⇑f : (a : A) → B) p.roots)
pos :
  ∀ (b : B) (h : Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) f) b),
    count b (map f p).roots = count b (Multiset.map (⇑f : (a : A) → B) p.roots)
⊢ Multiset.filter (fun (x : B) ↦ Membership.mem (γ := Subring B) (RingHom.range.{u_1, u_2} (R := A) f) x)
      (map f p).roots =
    Multiset.map (⇑f : (a : A) → B) p.roots
have neg : ∀ (b : B) (h : b ∉ RingHom.range.{u_1, u_2} (R := A) f), 0 = count b (Multiset.map (⇑f : (a : A) → B) p.roots)
Tactic: classical
  ext b
  rw [Multiset.count_filter]
  split_ifs with h
  · obtain ⟨a, rfl⟩ := h
    simp [hf, Multiset.count_map_eq_count', eq_rootMultiplicity_map hf]
  · refine (Multiset.count_eq_zero.mpr fun h' ↦ h ?_).symm
    exact Exists.imp (fun _ ↦ And.right) <| Multiset.mem_map.mp h'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsDomain A
inst_3 : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ p.roots.card ≤ (map f p).roots.card
have rw : Multiset.card.{u_2} (α := B) (Multiset.map (⇑f : (a : A) → B) p.roots) ≤ (map f p).roots.card
Tactic: rw [← p.roots.card_map f]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsDomain A
inst_3 : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ p.roots.card ≤ (map f p).roots.card
have pos : ∀ (hp0 : p = 0), p.roots.card ≤ (map f p).roots.card
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsDomain A
inst_3 : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
pos : ∀ (hp0 : p = 0), p.roots.card ≤ (map f p).roots.card
⊢ p.roots.card ≤ (map f p).roots.card
have neg : ∀ (hp0 : ¬p = 0), p.roots.card ≤ (map f p).roots.card
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Roots (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsDomain A
inst_3 : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hroots : p.roots.card = p.natDegree
⊢ Multiset.map (⇑f : (a : A) → B) p.roots = (map f p).roots
have apply : (map f p).roots.card ≤ Multiset.card.{u_2} (α := B) (Multiset.map (⇑f : (a : A) → B) p.roots)
Tactic: apply Multiset.eq_of_le_of_card_le (map_roots_le_of_injective p hf)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
d : ℕ
c : R
⊢ signVariations.{u_1} (R := R) ((monomial d : (a : R) → R[X]) c) = 0
have pos : ∀ (hcz : c = 0), signVariations.{u_1} (R := R) ((monomial d : (a : R) → R[X]) c) = 0
Tactic: by_cases hcz : c = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
d : ℕ
c : R
pos : ∀ (hcz : c = 0), signVariations.{u_1} (R := R) ((monomial d : (a : R) → R[X]) c) = 0
⊢ signVariations.{u_1} (R := R) ((monomial d : (a : R) → R[X]) c) = 0
have neg : ∀ (hcz : ¬c = 0), signVariations.{u_1} (R := R) ((monomial d : (a : R) → R[X]) c) = 0
Tactic: by_cases hcz : c = 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]
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
    ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType)
⊢ 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]
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
    ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType)
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 (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
    ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType)
hpz : ¬P = 0
⊢ P.eraseLead.signVariations = P.signVariations
have h₂ : P.nextCoeff ≠ 0
Tactic: have h₂ : nextCoeff P ≠ 0 := by intro; simp_all
-- 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 :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
    ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType)
hpz : ¬P = 0
h₂ : P.nextCoeff ≠ 0
⊢ P.eraseLead.signVariations = P.signVariations
have neg : ∀ (w : List R) (hl : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: w),
  P.eraseLead.signVariations = P.signVariations
Tactic: obtain ⟨_, hl⟩ := coeffList_eq_cons_leadingCoeff (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₂)
-- 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
⊢ P.signVariations =
    P.eraseLead.signVariations +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
have pos : ∀ (hpz : P = 0),
  P.signVariations =
    P.eraseLead.signVariations +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
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]
h : P ≠ 0
pos :
  ∀ (hpz : P = 0),
    P.signVariations =
      P.eraseLead.signVariations +
        if
            Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
              (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
          1
        else 0
⊢ P.signVariations =
    P.eraseLead.signVariations +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
have neg : ∀ (hpz : ¬P = 0),
  P.signVariations =
    P.eraseLead.signVariations +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
Tactic: by_cases hpz : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
⊢ P.signVariations =
    P.eraseLead.signVariations +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
have hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
Tactic: have hsl : SignType.sign (leadingCoeff P) ≠ 0 := by simp_all
-- 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)
⊢ P.signVariations =
    P.eraseLead.signVariations +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
have neg : 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.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.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.eraseLead.coeffList))) -
      1 +
    if
        Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
          (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
      1
    else 0
Tactic: rw [signVariations, signVariations, coeffList_eraseLead hpz]
-- 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)
⊢ 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.leadingCoeff ::
                (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.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.eraseLead.coeffList))) -
        1 +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
have neg : List.length (α := SignType)
      (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
          (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
            ((SignType.sign : (a : R) → SignType) P.leadingCoeff ::
              HAppend.hAppend (α := List SignType) (β := List SignType)
                (List.replicate (P.natDegree - P.eraseLead.degree.succ) ((SignType.sign : (a : R) → SignType) 0) :
                  List SignType)
                (List.map (⇑SignType.sign : (a : R) → SignType) P.eraseLead.coeffList : List SignType))) :
        List SignType) -
    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.eraseLead.coeffList))) -
      1 +
    if
        Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
          (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
      1
    else 0
Tactic: rw [List.map_cons, List.map_append, List.map_replicate]
-- 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)
⊢ List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
            (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
              ((SignType.sign : (a : R) → SignType) P.leadingCoeff ::
                HAppend.hAppend (α := List SignType) (β := List SignType)
                  (List.replicate (P.natDegree - P.eraseLead.degree.succ) ((SignType.sign : (a : R) → SignType) 0) :
                    List SignType)
                  (List.map (⇑SignType.sign : (a : R) → SignType) P.eraseLead.coeffList : List SignType))) :
          List SignType) -
      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.eraseLead.coeffList))) -
        1 +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
have neg : ∀ (h_eL : P.eraseLead.coeffList = []),
  List.length (α := SignType)
        (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
            (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
              ((SignType.sign : (a : R) → SignType) P.leadingCoeff ::
                HAppend.hAppend (α := List SignType) (β := List SignType)
                  (List.replicate (P.natDegree - P.eraseLead.degree.succ) ((SignType.sign : (a : R) → SignType) 0) :
                    List SignType)
                  (List.map.{u_1, 0} (α := R) (⇑SignType.sign : (a : R) → SignType) [] : List SignType))) :
          List SignType) -
      1 =
    List.length (α := SignType)
          (List.destutter (fun (x1 x2 : SignType) ↦ x1 ≠ x2)
            (List.filter (fun (x : SignType) ↦ decide (x ≠ 0))
              (List.map.{u_1, 0} (α := R) (⇑SignType.sign : (a : R) → SignType) []))) -
        1 +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
Tactic: rcases h_eL : P.eraseLead.coeffList with _ | ⟨c, cs⟩
-- 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)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₂ : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
⊢ False
have suffices : P.eraseLead = 0
Tactic: suffices eraseLead P = 0 by grind [coeffList_zero]
-- 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)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₂ : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
⊢ P.eraseLead = 0
have by_contra : ∀ (h : ¬P.eraseLead = 0), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
h_1 : P ≠ 0
hpz : ¬P = 0
hsl : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₂ : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
h : ¬P.eraseLead = 0
⊢ False
have this : ∃ (ls : List R), P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: ls
Tactic: have := coeffList_eq_cons_leadingCoeff h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.RuleOfSigns (hypothesis)
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)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
⊢ c = P.eraseLead.leadingCoeff
have h_eL₁ : P.eraseLead ≠ 0
Tactic: have h_eL : eraseLead P ≠ 0 := by simp [← coeffList_eq_nil, h_eL]
-- 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)
c : R
cs : List R
h_eL_1 : P.eraseLead.coeffList = c :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
h_eL : P.eraseLead ≠ 0
⊢ c = P.eraseLead.leadingCoeff
have obtain : ∀ (ls : List R) (hls : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: ls), c = P.eraseLead.leadingCoeff
Tactic: obtain ⟨ls, hls⟩ := coeffList_eq_cons_leadingCoeff h_eL
-- 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)
⊢ List.length (α := SignType)
        (if
              ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
                  ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
            (SignType.sign : (a : R) → SignType) P.leadingCoeff ::
              List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
                ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff)
                (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) ((SignType.sign : (a : R) → SignType) P.leadingCoeff)
              (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
          List SignType) -
      1 =
    List.length (α := SignType)
          (List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
              ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff)
              (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
            List SignType) -
        1 +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
have neg : List.length (α := SignType)
      ((SignType.sign : (a : R) → SignType) P.leadingCoeff ::
          List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
            ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff)
            (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType) -
    1 =
  List.length (α := SignType)
        (List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
            ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff)
            (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
          List SignType) -
      1 +
    1
Tactic: rw [if_pos h₄, if_pos ?_]
-- 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)
neg :
  List.length (α := SignType)
        ((SignType.sign : (a : R) → SignType) P.leadingCoeff ::
            List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
              ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff)
              (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
          List SignType) -
      1 =
    List.length (α := SignType)
          (List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
              ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff)
              (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
            List SignType) -
        1 +
      1
⊢ List.length (α := SignType)
        (if
              ¬Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
                  ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
            (SignType.sign : (a : R) → SignType) P.leadingCoeff ::
              List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
                ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff)
                (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) ((SignType.sign : (a : R) → SignType) P.leadingCoeff)
              (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
          List SignType) -
      1 =
    List.length (α := SignType)
          (List.destutter' (fun (x1 x2 : SignType) ↦ ¬x1 = x2)
              ((SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff)
              (List.filter (fun (x : SignType) ↦ !decide (x = 0)) (List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
            List SignType) -
        1 +
      if
          Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
            (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType) then
        1
      else 0
have rw : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
  (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
Tactic: rw [if_pos h₄, if_pos ?_]
-- 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)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType)
    (-(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff : SignType)
have zero : (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.zero →
  SignType.zero = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff
Tactic: cases _ : SignType.sign P.leadingCoeff