awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Roots
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
neg : ∀ (hp0 : ¬p = 0), p.roots.card ≤ (map f p).roots.card
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.Algebra.Polynomial.Roots
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)
hp0 : p = 0
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
simp only [hp0, roots_zero, Polynomial.map_zero, Multiset.card_zero, le_rfl]

Premises used: le_rfl, Polynomial.roots_zero, Multiset.card_zero, Polynomial.map_zero
-- Module: Mathlib.Algebra.Polynomial.Roots
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)
hp0 : ¬p = 0
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
card_roots_le_map ((Polynomial.map_ne_zero_iff hf).mpr hp0)

Premises used: Iff.mpr, Polynomial.card_roots_le_map, Polynomial.map_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Roots
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)
hp0 : ¬p = 0
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
exact card_roots_le_map ((Polynomial.map_ne_zero_iff hf).mpr hp0)

Premises used: Iff.mpr, Polynomial.card_roots_le_map, Polynomial.map_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Roots
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
apply : (map f p).roots.card ≤ Multiset.card.{u_2} (α := B) (Multiset.map (⇑f : (a : A) → B) p.roots)
⊢ Multiset.map (⇑f : (a : A) → B) p.roots = (map f p).roots

Tactic:
apply Multiset.eq_of_le_of_card_le (map_roots_le_of_injective p hf)

Premises used: Polynomial.map_roots_le_of_injective, Multiset.eq_of_le_of_card_le
-- Module: Mathlib.Algebra.Polynomial.Roots
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
⊢ (map f p).roots.card ≤ Multiset.card.{u_2} (α := B) (Multiset.map (⇑f : (a : A) → B) p.roots)

Tactic:
simpa only [Multiset.card_map, hroots] using card_roots_map_le_natDegree p

Premises used: Polynomial.card_roots_map_le_natDegree, Multiset.card_map
-- Module: Mathlib.Algebra.Polynomial.Roots
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
hroots : p.roots.card = p.natDegree
⊢ (map f p).roots.card ≤ Multiset.card.{u_2} (α := B) (Multiset.map (⇑f : (a : A) → B) p.roots)

Tactic:
simpa only [Multiset.card_map, hroots] using card_roots_map_le_natDegree p

Premises used: Polynomial.card_roots_map_le_natDegree, Multiset.card_map
-- Module: Mathlib.Algebra.Polynomial.Roots
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]
hm : p.Monic
f : A →+* B
hroots : p.roots.card = p.natDegree
⊢ Multiset.map (⇑f : (a : A) → B) p.roots = (Polynomial.map f p).roots

Tactic:
roots_map_of_map_ne_zero_of_card_eq_natDegree f (map_monic_ne_zero hm) hroots

Premises used: Polynomial.map_monic_ne_zero, Polynomial.roots_map_of_map_ne_zero_of_card_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
⊢ signVariations.{u_1} (R := R) 0 = 0

Tactic:
simp [signVariations]

Premises used: Polynomial.signVariations
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
neg : ∀ (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

Tactic:
by_cases hcz : c = 0
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
d : ℕ
c : R
hcz : c = 0
⊢ signVariations.{u_1} (R := R) ((monomial d : (a : R) → R[X]) c) = 0

Tactic:
simp [hcz]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
d : ℕ
c : R
hcz : ¬c = 0
⊢ signVariations.{u_1} (R := R) ((monomial d : (a : R) → R[X]) c) = 0

Tactic:
simp [hcz, signVariations, coeffList_eraseLead (mt (monomial_eq_zero_iff c d).mp hcz)]

Premises used: Polynomial.signVariations, Polynomial.monomial_eq_zero_iff, Polynomial.coeffList_eraseLead, mt, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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]
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

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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_1 : P.nextCoeff = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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.nextCoeff ≠ 0

Tactic:
have h₂ : nextCoeff P ≠ 0 := by intro; simp_all
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
neg :
  ∀ (w : List R) (hl : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: w),
    P.eraseLead.signVariations = P.signVariations
⊢ P.eraseLead.signVariations = P.signVariations

Tactic:
obtain ⟨_, hl⟩ := coeffList_eq_cons_leadingCoeff (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₂)

Premises used: Polynomial.coeffList_eq_cons_leadingCoeff, mt, Polynomial.nextCoeff_eq_zero_of_eraseLead_eq_zero
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
w : List R
hl : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: w
⊢ P.eraseLead.signVariations = P.signVariations

Tactic:
simp [signVariations, List.destutter, leadingCoeff_eraseLead_eq_nextCoeff h₂, hl, h, h₂,
      coeffList_eraseLead hpz]

Premises used: Polynomial.signVariations, Polynomial.coeffList_eraseLead, List.destutter, Polynomial.leadingCoeff_eraseLead_eq_nextCoeff
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
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
⊢ 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
-- 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
⊢ 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:
simp_all
-- 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
⊢ Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)

Tactic:
simp_all
-- 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
⊢ Ne (α := SignType) ((SignType.sign : (a : R) → SignType) P.leadingCoeff : SignType) (0 : SignType)

Tactic:
have hsl : SignType.sign (leadingCoeff P) ≠ 0 := by simp_all
-- 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)
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
⊢ 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:
rw [signVariations, signVariations, coeffList_eraseLead hpz]

Premises used: Polynomial.signVariations, Polynomial.coeffList_eraseLead
-- 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)
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
⊢ 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 [List.map_cons, List.map_append, List.map_replicate]

Premises used: List.map_cons, List.map_append, List.map_replicate
-- 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)
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:
simp [coeffList_eq_nil.mp h_eL, h]

Premises used: Polynomial.coeffList_eq_nil, Iff.mp
-- 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)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
by_contra : ∀ (h₂ : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)), False
⊢ Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)

Tactic:
by_contra h₂
-- 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)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₂ : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
this : P.eraseLead = 0
⊢ False

Tactic:
grind [coeffList_zero]

Premises used: Polynomial.coeffList_zero
-- 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)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₂ : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
suffices : P.eraseLead = 0
⊢ False

Tactic:
suffices eraseLead P = 0 by grind [coeffList_zero]
-- 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)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₂ : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
by_contra : ∀ (h : ¬P.eraseLead = 0), False
⊢ P.eraseLead = 0

Tactic:
by_contra h
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
⊢ ∃ (ls : List R), P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: ls

Tactic:
have := coeffList_eq_cons_leadingCoeff h
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
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
this : ∃ (ls : List R), P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: ls
⊢ False

Tactic:
grind [leadingCoeff_eq_zero, sign_eq_zero_iff]

Premises used: sign_eq_zero_iff, Polynomial.leadingCoeff_eq_zero
-- 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)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
⊢ Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)

Tactic:
have h₁ : SignType.sign c ≠ 0 := by
    by_contra h₂
    suffices eraseLead P = 0 by grind [coeffList_zero]
    by_contra h
    have := coeffList_eq_cons_leadingCoeff h
    grind [leadingCoeff_eq_zero, sign_eq_zero_iff]
-- 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)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
⊢ P.eraseLead ≠ 0

Tactic:
simp [← coeffList_eq_nil, h_eL]

Premises used: Polynomial.coeffList_eq_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)
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₁ : Ne (α := SignType) ((SignType.sign : (a : R) → SignType) c : SignType) (0 : SignType)
⊢ P.eraseLead ≠ 0

Tactic:
have h_eL : eraseLead P ≠ 0 := by simp [← coeffList_eq_nil, h_eL]
-- 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)
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
obtain : ∀ (ls : List R) (hls : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: ls), c = P.eraseLead.leadingCoeff
⊢ c = P.eraseLead.leadingCoeff

Tactic:
obtain ⟨ls, hls⟩ := coeffList_eq_cons_leadingCoeff h_eL

Premises used: Polynomial.coeffList_eq_cons_leadingCoeff
-- 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)
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
ls : List R
hls : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: ls
⊢ c = P.eraseLead.leadingCoeff

Tactic:
grind
-- 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)
        (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:
grind [SignType.neg_eq_self_iff]

Premises used: SignType.neg_eq_self_iff