mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ (SignType.sign P.leadingCoeff ::
          List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
        1 +
      1

pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ (SignType.sign P.leadingCoeff ::
          List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
        1 +
      1

R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ 0 ≤ p.natDegree - q ∧ ∀ x ∈ range (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ 0 ≤ p.natDegree - q ∧ ∀ x ∈ range (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (g j) ∧ IsCoprime (g i) (∏ x ∈ s, g x)

Tactic:
]

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ IsCoprime (g i) (g j) ∧ IsCoprime (g i) (∏ x ∈ s, g x)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
⊢ ∑ x ∈ range (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = q ! • (aeval r) ((range (p.natDegree + 1)).sum c)

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
⊢ ∑ x ∈ range (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = q ! • (aeval r) ((range (p.natDegree + 1)).sum c)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (List.map (⇑SignType.sign) (List.map (fun x ↦ -x) P.coeffList)))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (List.map (⇑SignType.sign) (List.map (fun x ↦ -x) P.coeffList)))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
hsc : (⇑SignType.sign ∘ fun x ↦ -x) = (fun x ↦ -x) ∘ ⇑SignType.sign
h_neg_destutter :
  ∀ (l : List SignType),
    List.map (fun x ↦ -x) (List.destutter (fun x1 x2 ↦ ¬x1 = x2) l) =
      List.destutter (fun x1 x2 ↦ ¬x1 = x2) (List.map (fun x ↦ -x) l)
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (List.map (⇑SignType.sign)
            (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ (fun x ↦ -x) ∘ ⇑SignType.sign) P.coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign) (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign) P.coeffList))).length -
      1

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
hsc : (⇑SignType.sign ∘ fun x ↦ -x) = (fun x ↦ -x) ∘ ⇑SignType.sign
h_neg_destutter :
  ∀ (l : List SignType),
    List.map (fun x ↦ -x) (List.destutter (fun x1 x2 ↦ ¬x1 = x2) l) =
      List.destutter (fun x1 x2 ↦ ¬x1 = x2) (List.map (fun x ↦ -x) l)
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (List.map (⇑SignType.sign)
            (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ (fun x ↦ -x) ∘ ⇑SignType.sign) P.coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign) (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
hf :
  q₁ * (g i * ∏ x ∈ s, g x) + (r₁ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₁ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k) =
    q₂ * (g i * ∏ x ∈ s, g x) + (r₂ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₂ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k)
cop : IsCoprime (g i) (∏ i ∈ s, g i)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
]

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
hf :
  q₁ * (g i * ∏ x ∈ s, g x) + (r₁ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₁ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k) =
    q₂ * (g i * ∏ x ∈ s, g x) + (r₂ i * ∏ k ∈ s, g k + ∑ x ∈ s, r₂ x * ∏ k ∈ (Finset.cons i s hi).erase x, g k)
cop : IsCoprime (g i) (∏ i ∈ s, g i)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
inst✝³ : LinearOrder R✝
η✝ : R✝
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
P : R[X]
hx : η ≠ 0
hx2 : 0 < η
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) (C η * P).coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1

Tactic:
]

Goal state after:
R✝ : Type u_1
inst✝⁴ : Ring R✝
inst✝³ : LinearOrder R✝
η✝ : R✝
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
P : R[X]
hx : η ≠ 0
hx2 : 0 < η
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) (C η * P).coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
inst✝³ : LinearOrder R✝
η✝ : R✝
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
P : R[X]
hx : η ≠ 0
hx2 : 0 < η
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign ∘ fun x ↦ η * x) P.coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1

Tactic:
]

Goal state after:
R✝ : Type u_1
inst✝⁴ : Ring R✝
inst✝³ : LinearOrder R✝
η✝ : R✝
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
P : R[X]
hx : η ≠ 0
hx2 : 0 < η
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign ∘ fun x ↦ η * x) P.coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
⊢ 0 ≤ 0 - q ∧
    ∀ (r : A) {p' : A[X]},
      map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p' →
        (aeval r) (sumIDeriv 0) = (q - 1)! • eval r p' + q ! • (aeval r) 0

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
⊢ 0 ≤ 0 - q ∧
    ∀ (r : A) {p' : A[X]},
      map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p' →
        (aeval r) (sumIDeriv 0) = (q - 1)! • eval r p' + q ! • (aeval r) 0
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hPn0 : P ≠ 0
⊢ P.natDegree + 1 = P.natDegree + 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hePn0 : P.eraseLead ≠ 0
⊢ P.eraseLead.natDegree + 1 = P.natDegree

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hePn0 : P.eraseLead ≠ 0
⊢ P.eraseLead.natDegree + 1 = P.natDegree
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
⊢ P.coeff d < η * P.coeff (d + 1)

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
⊢ P.coeff d < η * P.coeff (d + 1)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case right
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p'
⊢ 0 = (q - 1)! • eval r p'

Tactic:
]

Goal state after:
case right
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : map (algebraMap R A) 0 = (X - C r) ^ (q - 1) * p'
⊢ 0 = (q - 1)! • eval r p'
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
⊢ ((X - C η) * P).natDegree = ((X - C η) * P).natDegree

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case right
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : 0 = (X - C r) ^ (q - 1) * p'
⊢ 0 = (q - 1)! • eval r p'

Tactic:
]

Goal state after:
case right
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : 0 = (X - C r) ^ (q - 1) * p'
⊢ 0 = (q - 1)! • eval r p'
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
this✝ : ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead
this :
  List.map (⇑SignType.sign) ((X - C η) * P).eraseLead.coeffList =
    List.map (⇑SignType.sign) ((X - C η) * P.eraseLead).coeffList
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (List.map (⇑SignType.sign) ((X - C η) * P.eraseLead).coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (List.map (⇑SignType.sign) ((X - C η) * P.eraseLead).coeffList))).length -
      1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case right.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : p' = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  r₁ i * ∏ x ∈ s, g x + g i * (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x) =
    r₂ i * ∏ x ∈ s, g x + g i * (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
]

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hf :
  r₁ i * ∏ x ∈ s, g x + g i * (q₁ * ∏ x ∈ s, g x + ∑ i ∈ s, r₁ i * ∏ x ∈ s.erase i, g x) =
    r₂ i * ∏ x ∈ s, g x + g i * (q₂ * ∏ x ∈ s, g x + ∑ i ∈ s, r₂ i * ∏ x ∈ s.erase i, g x)
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m < n

Tactic:
]

Goal state after:
case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m < n
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ ((X - C η) * P).eraseLead - (monomial ((X - C η) * P).eraseLead.natDegree) ((X - C η) * P).nextCoeff =
    ((X - C η) * P.eraseLead).eraseLead

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ ((X - C η) * P).eraseLead - (monomial ((X - C η) * P).eraseLead.natDegree) ((X - C η) * P).nextCoeff =
    ((X - C η) * P.eraseLead).eraseLead
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
k : ℕ
h : ¬q ≤ k
⊢ 0 ≤ p.natDegree - k

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
k : ℕ
h : ¬q ≤ k
⊢ 0 ≤ p.natDegree - k