awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h₇ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
h₈ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead =
    HSub.hSub (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead)
      ((monomial P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
this_1 :
  P.eraseLead.natDegree + 2 =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList.length
this_2 : P.natDegree + 2 = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).coeffList.length
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff = P.leadingCoeff
h₉ : ¬(HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff = 0
⊢ (monomial P.natDegree : (a : R) → R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    HSub.hSub (α := R[X]) ((monomial P.natDegree : (a : R) → R[X]) P.nextCoeff : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) η : R[X])
        ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff : R[X]))

Tactic:
grind [coeff_X_sub_C_mul, nextCoeff_of_natDegree_pos, leadingCoeff]

Premises used: Polynomial.nextCoeff_of_natDegree_pos, Polynomial.coeff_X_sub_C_mul, Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList) =
    P.nextCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h₇ :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X])).leadingCoeff * P.eraseLead.leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList) =
    P.nextCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h₈ :
  1 * P.eraseLead.leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList) =
    P.nextCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h₉ :
  P.eraseLead.leadingCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList) =
    P.nextCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
h₁₀ h₁₁ :
  P.nextCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList) =
    P.nextCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).coeffList =
    P.nextCoeff ::
      (List.replicate n 0 ++
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).eraseLead.coeffList)

Tactic:
rw [h_cons, leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, h₂]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.leadingCoeff_X_sub_C, one_mul
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
obtain :
  ∀ (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),
    (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).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).signVariations

Tactic:
obtain ⟨c₀, cs, ⟨hcs, hecs⟩⟩ := exists_cons_of_leadingCoeff_pos η h h₂.ne'

Premises used: LT.lt.ne', _private.0.Polynomial.exists_cons_of_leadingCoeff_pos
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
simp :
  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))
            ((SignType.sign : (a : R) → SignType) c₀ :: List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)
⊢ (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).signVariations

Tactic:
simp +decide only [hcs, hecs, h, h₂, signVariations, List.destutter, List.map_cons, sign_pos,
    List.filter_cons_of_pos, tsub_le_iff_right,
    Nat.sub_add_cancel (List.length_pos_of_ne_nil (List.destutter'_ne_nil _ _))]

Premises used: List.filter_cons_of_pos, List.map_cons, Polynomial.signVariations, sign_pos, List.destutter, tsub_le_iff_right, Nat.sub_add_cancel, List.length_pos_of_ne_nil, Decidable.decide, List.destutter'_ne_nil
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
rw :
  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)
⊢ 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))
            ((SignType.sign : (a : R) → SignType) c₀ :: List.map (⇑SignType.sign : (a : R) → SignType) cs)) :
        List SignType)

Tactic:
rw [List.filter_cons]

Premises used: List.filter_cons
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
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)))
⊢ 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)

Tactic:
split
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
      (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:
rfl
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
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)))
⊢ 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)

Tactic:
split
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
      (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:
rfl
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
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)
⊢ 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:
rcases hcs : (cs.map SignType.sign).filter fun x ↦ decide (x ≠ 0) with _ | ⟨r, rs⟩

Premises used: List.map, Ne, List.filter, OfNat.ofNat, Decidable.decide, DFunLike.coe, SignType.sign
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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_1 : (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)
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:
simp
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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_1 : (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)
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:
grind [List.destutter_cons_cons]

Premises used: List.destutter_cons_cons
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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
⊢ 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

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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
⊢ 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

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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 :
  ∀ {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 ≠ 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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 :
  ∀ {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).natDegree = d

Tactic:
simpa