awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
rw :
  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

Tactic:
rw [if_pos h₄, if_pos ?_]

Premises used: if_pos
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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)
        ((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:
grind [Nat.sub_add_cancel, List.length_pos_of_ne_nil, List.destutter'_ne_nil]

Premises used: Nat.sub_add_cancel, List.length_pos_of_ne_nil, List.destutter'_ne_nil
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
pos :
  (SignType.sign : (a : R) → SignType) P.leadingCoeff = SignType.pos →
    SignType.pos = -(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)

Tactic:
cases _ : SignType.sign P.leadingCoeff

Premises used: Polynomial.leadingCoeff, DFunLike.coe, SignType.sign
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
zero₂ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.pos → SignType.zero = -SignType.pos
⊢ SignType.zero = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff

Tactic:
cases _ : SignType.sign P.eraseLead.leadingCoeff

Premises used: Polynomial.leadingCoeff, Polynomial.eraseLead, DFunLike.coe, SignType.sign
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
neg₂ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.pos → SignType.neg = -SignType.pos
⊢ SignType.neg = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff

Tactic:
cases _ : SignType.sign P.eraseLead.leadingCoeff

Premises used: Polynomial.leadingCoeff, Polynomial.eraseLead, DFunLike.coe, SignType.sign
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
pos₂ : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.pos → SignType.pos = -SignType.pos
⊢ SignType.pos = -(SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff

Tactic:
cases _ : SignType.sign P.eraseLead.leadingCoeff

Premises used: Polynomial.leadingCoeff, Polynomial.eraseLead, DFunLike.coe, SignType.sign
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
h_2 : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero
⊢ SignType.zero = -SignType.zero

Tactic:
grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

Premises used: SignType.neg_eq_neg_one, neg_neg, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
h_2 : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.neg
⊢ SignType.zero = -SignType.neg

Tactic:
grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

Premises used: SignType.neg_eq_neg_one, neg_neg, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
h_2 : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.pos
⊢ SignType.zero = -SignType.pos

Tactic:
grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

Premises used: SignType.neg_eq_neg_one, neg_neg, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
h_2 : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero
⊢ SignType.neg = -SignType.zero

Tactic:
grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

Premises used: SignType.neg_eq_neg_one, neg_neg, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
h_2 : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.neg
⊢ SignType.neg = -SignType.neg

Tactic:
grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

Premises used: SignType.neg_eq_neg_one, neg_neg, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
h_2 : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.pos
⊢ SignType.neg = -SignType.pos

Tactic:
grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

Premises used: SignType.neg_eq_neg_one, neg_neg, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
h_2 : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.zero
⊢ SignType.pos = -SignType.zero

Tactic:
grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

Premises used: SignType.neg_eq_neg_one, neg_neg, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
h_2 : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.neg
⊢ SignType.pos = -SignType.neg

Tactic:
grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

Premises used: SignType.neg_eq_neg_one, neg_neg, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
h_2 : (SignType.sign : (a : R) → SignType) P.eraseLead.leadingCoeff = SignType.pos
⊢ SignType.pos = -SignType.pos

Tactic:
grind [= SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one,
      SignType.neg_eq_neg_one, neg_neg]

Premises used: SignType.neg_eq_neg_one, neg_neg, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
pos : ∀ (hpz : P = 0), P.eraseLead.signVariations ≤ P.signVariations
neg : ∀ (hpz : ¬P = 0), P.eraseLead.signVariations ≤ P.signVariations
⊢ P.eraseLead.signVariations ≤ P.signVariations

Tactic:
by_cases hpz : P = 0
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
hpz : P = 0
⊢ P.eraseLead.signVariations ≤ P.signVariations

Tactic:
simp [hpz]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
hpz : ¬P = 0
⊢ P.eraseLead.signVariations ≤ P.signVariations

Tactic:
grind [signVariations_eq_eraseLead_add_ite]

Premises used: Polynomial.signVariations_eq_eraseLead_add_ite
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
neg : ∀ (hpz : ¬P = 0), P.signVariations ≤ P.eraseLead.signVariations + 1
⊢ P.signVariations ≤ P.eraseLead.signVariations + 1

Tactic:
by_cases hpz : P = 0
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
hpz : P = 0
⊢ P.signVariations ≤ P.eraseLead.signVariations + 1

Tactic:
simp [hpz]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
P : R[X]
hpz : ¬P = 0
⊢ P.signVariations ≤ P.eraseLead.signVariations + 1

Tactic:
grind [signVariations_eq_eraseLead_add_ite]

Premises used: Polynomial.signVariations_eq_eraseLead_add_ite
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
P : R[X]
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
⊢ (-P).signVariations = P.signVariations

Tactic:
rw [signVariations, signVariations, coeffList_neg]

Premises used: Polynomial.signVariations, Polynomial.coeffList_neg
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
P : R[X]
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
⊢ 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:
simp only [List.map_map, List.filter_map]

Premises used: List.filter_map, List.map_map
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
P : R[X]
⊢ 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:
grind [Left.sign_neg]

Premises used: Left.sign_neg
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
P : R[X]
⊢ 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]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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))
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:
grind [List.map_destutter, neg_inj]

Premises used: List.map_destutter, neg_inj