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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ eval x (C (eval y p)) = eval y p

Tactic:
eval_C

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ eval y p = eval y p
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y p : R
⊢ eval x (C p) = p

Tactic:
eval_C

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y p : R
⊢ p = p
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
⊢ eval x (C y) = y

Tactic:
eval_C

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
⊢ y = y
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) + (r.divModByMonicAux hq).1.coeff i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (r.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
have deg_r_lt_deg_p : deg(r) < deg(p) := natDegree_lt_natDegree hr' (hr ▸ div_wf_lemma hpq hq)

Goal state after:
case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) + (r.divModByMonicAux hq).1.coeff i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (r.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
⊢ (p.comp q).IsMonicOfDegree (m * n)

Tactic:
by
  rcases subsingleton_or_nontrivial R with h | h
  · simp only [isMonicOfDegree_iff_of_subsingleton, mul_eq_zero] at hp ⊢
    exact .inl hp
  rw [← hp.natDegree_eq, ← hq.natDegree_eq]
  refine (isMonicOfDegree_iff ..).mpr ⟨natDegree_comp_le, ?_⟩
  rw [coeff_comp_degree_mul_degree (hq.natDegree_eq ▸ hn), hp.leadingCoeff_eq, hq.leadingCoeff_eq,
    one_pow, one_mul]

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

Goal state before:
pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) + (r.divModByMonicAux hq).1.coeff i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (r.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
refine ⟨add_mem ?_ ?_, ?_⟩

Goal state after:
case neg.refine_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

case neg.refine_2
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
⊢ (r.divModByMonicAux hq).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

case neg.refine_3
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
⊢ (r.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ i (r * a ^ n * b ^ (N - n)) = i b ^ N * (eval (i a * bi) (C (i r)) * eval (i a * bi) X ^ n)

Tactic:
eval_C

Goal state after:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ i (r * a ^ n * b ^ (N - n)) = i b ^ N * (i r * eval (i a * bi) X ^ n)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ (p i * ∏ i ∈ s, p i).homogenize (n i + ∑ i ∈ s, n i) = (p i).homogenize (n i) * ∏ i ∈ s, (p i).homogenize (n i)

Tactic:
homogenize_mul _ _ h.1,

Goal state after:
case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ (p i).homogenize (n i) * (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) =
    (p i).homogenize (n i) * ∏ i ∈ s, (p i).homogenize (n i)

case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ (∏ i ∈ s, p i).natDegree ≤ ∑ i ∈ s, n i
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
⊢ (b :: destutter' R c l).length ≤ (a :: destutter' R c l).length

Tactic:
length_cons,

Goal state after:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
⊢ (destutter' R c l).length + 1 ≤ (destutter' R c l).length + 1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ fold max 0 (natDegree ∘ fun i ↦ C ((i + k).choose k • p.coeff (i + k)) * X ^ i) ((⇑derivative)^[k] p).support ≤
    p.natDegree - k

Tactic:
rw [fold_max_le]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ 0 ≤ p.natDegree - k ∧
    ∀ x ∈ ((⇑derivative)^[k] p).support,
      (natDegree ∘ fun i ↦ C ((i + k).choose k • p.coeff (i + k)) * X ^ i) x ≤ p.natDegree - k
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
x : ℕ
⊢ (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)

Tactic:
rw [← pow_add, add_tsub_cancel_of_le]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
x : ℕ
⊢ 1 ≤ q - (k - x)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
x : ℕ
h : 1 ≤ x
h' : x ≤ q
⊢ (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)

Tactic:
rw [← pow_add, add_tsub_cancel_of_le]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
x : ℕ
h : 1 ≤ x
h' : x ≤ q
⊢ 1 ≤ q - (q - x)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
use 0

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : k < q
⊢ natDegree 0 ≤ p.natDegree - q ∧
    ∀ (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) 0
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)
⊢ fold max 0 (natDegree ∘ c) (range (p.natDegree + 1)) ≤ p.natDegree - q

Tactic:
rw [fold_max_le]

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.SumIteratedDerivative

Goal state before:
pp: case inl
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)
⊢ ∃ gp,
    gp.natDegree ≤ natDegree 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) gp

Tactic:
use 0

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)
⊢ natDegree 0 ≤ natDegree 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.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]},
    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:
intro r p' hp

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'
⊢ (aeval r) (sumIDeriv 0) = (q - 1)! • eval r p' + q ! • (aeval r) 0
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_1
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
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ fold max 0 (natDegree ∘ c) (Ico q (p.natDegree + 1)) ≤ p.natDegree - q

Tactic:
rw [fold_max_le]

Goal state after:
case inr.refine_1
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
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ 0 ≤ p.natDegree - q ∧ ∀ x ∈ Ico q (p.natDegree + 1), (natDegree ∘ c) x ≤ p.natDegree - q
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.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
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
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ∀ (r : A) {p' : A[X]},
    map (algebraMap R A) p = (X - C r) ^ (q - 1) * p' →
      (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)

Tactic:
intro r p' hp

Goal state after:
case inr.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
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
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (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 - 1) * p'
⊢ (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) (∑ x ∈ Ico q (p.natDegree + 1), c x)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case h.left
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
have h₇ : natDegree ((X - C η) * P) = P.natDegree + 1 := by
      rw [natDegree_mul h₅ h₃, natDegree_X_sub_C, add_comm]

Goal state after:
case h.left
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
⊢ ((X - C η) * P).coeffList =
    P.leadingCoeff :: ((X - C η) * P).nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q.mirror = p ∨ q.mirror = p.mirror

Tactic:
exact
      irreducible_aux2 hkm hmn (lt_add_of_pos_left k (tsub_pos_of_lt hmn'))
        (lt_tsub_iff_right.mp ((tsub_lt_tsub_iff_left_of_le hmn'.le).mpr hkm')) u v w hp hq h

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 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (if decide (SignType.sign c₀ ≠ 0) = true then
          SignType.sign c₀ :: List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs)
        else List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

Tactic:
split

Goal state after:
case isTrue
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝ : decide (SignType.sign c₀ ≠ 0) = true
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (SignType.sign c₀ :: List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

case isFalse
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝ : ¬decide (SignType.sign c₀ ≠ 0) = true
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case isTrue
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝ : decide (SignType.sign c₀ ≠ 0) = true
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (if 1 ≠ SignType.sign c₀ then
        1 ::
          List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀)
            (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))
      else
        List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

Tactic:
split

Goal state after:
case isTrue.isTrue
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : 1 ≠ SignType.sign c₀
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (1 ::
        List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀)
          (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length

case isTrue.isFalse
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : ¬1 ≠ SignType.sign c₀
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih : ∀ m < d, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
have h_deg_mul : natDegree ((X - C η) * P) = natDegree P + 1 := by
    rw [natDegree_mul (X_sub_C_ne_zero η) hP, natDegree_X_sub_C, add_comm]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
d : ℕ
ih : ∀ m < d, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
P : R[X]
hP : P ≠ 0
hd : P.natDegree = d
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations