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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ (m + k).succ.descFactorial k • p.coeff (m + k).succ * (↑m + 1) =
    (m + k).succ.descFactorial k • p.coeff (m + k).succ * (↑m + 1)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ eval₂ ((algebraMap A B).comp (algebraMap R A)) x p = eval₂ ((algebraMap A B).comp (algebraMap R A)) x p

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
⊢ eval₂ (algebraMap R B) ((algebraMap A B) x) p = eval₂ (algebraMap R B) ((algebraMap A B) x) p

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : IsTorsionFree A B
inst✝ : Nontrivial B
x : A
p : R[X]
⊢ (aeval x) p = 0 ↔ (aeval x) p = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective ⇑(algebraMap A B)
⊢ (aeval x) p = 0 ↔ (aeval x) p = 0

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree < q.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ map f p = map f p

Tactic:
]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ 1 ≠ 0

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this : Nontrivial R
⊢ 1 ≠ 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ 0 = 0

pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ 0 ∈ Multiset.map (⇑(aeval x)) (Multiset.map (fun x ↦ X - C x) s)

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ 0 ∈ Multiset.map (⇑(aeval x)) (Multiset.map (fun x ↦ X - C x) s)
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ ∃ a ∈ s, (⇑(aeval x) ∘ fun x ↦ X - C x) a = 0

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ ∃ a ∈ s, (⇑(aeval x) ∘ fun x ↦ X - C x) a = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
⊢ q ∣ q * (p /ₘ q)

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
⊢ q ∣ q * (p /ₘ q)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((m + 1) * (m.succ + k).descFactorial k) • p.coeff (m + k.succ) =
    (m.succ * (m.succ + k).descFactorial k) • p.coeff (m + k.succ)

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ p - q * (p /ₘ q) = p - q * (p /ₘ q)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∑ a ∈ range p.natDegree.succ, g ((s • p).coeff a) * x ^ a = g s * ∑ a ∈ range p.natDegree.succ, g (p.coeff a) * x ^ a

pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0

pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∑ a ∈ range p.natDegree.succ, g ((s • p).coeff a) * x ^ a = g s * ∑ a ∈ range p.natDegree.succ, g (p.coeff a) * x ^ a

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
g : R →+* S
p : R[X]
x : S
s : R
A : p.natDegree < p.natDegree.succ
B : (s • p).natDegree < p.natDegree.succ
⊢ ∀ (n : ℕ), g 0 * x ^ n = 0
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
x : R
⊢ s • eval x p = s • eval x p

Tactic:
]

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

Goal state before:
pp: case neg.a.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ q.natDegree ≤ q.natDegree

pp: case neg.a.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ p.natDegree ≤ q.natDegree

Tactic:
]

Goal state after:
case neg.a.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ p.natDegree ≤ q.natDegree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ) = (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ s • eval₂ C q p = s • eval₂ C q p

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h✝ : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
r : R
⊢ f r • eval₂ (C.comp f) X p = f r • eval₂ (C.comp f) X p

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C ((k ! * (i + k).choose k) • p.coeff (i + k)) * X ^ i = C ((k ! * (i + k).choose k) • p.coeff (i + k)) * X ^ i

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
⊢ (r - p /ₘ q).leadingCoeff ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
⊢ (r - p /ₘ q).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ (C p.leadingCoeff * q +
          -(C q.leadingCoeff * (p * X ^ (p.natDegree + (q.natDegree - p.natDegree) - p.natDegree)))).coeff
      (p.natDegree + (q.natDegree - p.natDegree)) =
    0

Tactic:
]

Goal state after:
case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ (C p.leadingCoeff * q +
          -(C q.leadingCoeff * (p * X ^ (p.natDegree + (q.natDegree - p.natDegree) - p.natDegree)))).coeff
      (p.natDegree + (q.natDegree - p.natDegree)) =
    0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : ↑q.natDegree + ↑(r - p /ₘ q).natDegree < ↑q.natDegree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : ↑q.natDegree + ↑(r - p /ₘ q).natDegree < ↑q.natDegree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ p ∣ p

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ q ∣ q * p

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ q ∣ q * p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f (y %ₘ x) = 0 ↔ y %ₘ x = 0

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
⊢ map f (y %ₘ x) = 0 ↔ y %ₘ x = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
H : map f (y %ₘ x) = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    ∑ x ∈ ((⇑derivative)^[k] p).support, k ! • (C ((x + k).choose k • p.coeff (x + k)) * X ^ x)

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    ∑ x ∈ ((⇑derivative)^[k] p).support, k ! • (C ((x + k).choose k • p.coeff (x + k)) * X ^ x)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
H : y %ₘ x = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ q * p = q * p

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ ⊥ < q.degree

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ ⊥ < q.degree
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : (C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).natDegree = q.natDegree
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
⊢ (p.cancelLeads q).natDegree < q.natDegree

Tactic:
by_cases hp : p = 0
  · convert! hq
    simp [hp, cancelLeads]
  rw [cancelLeads, sub_eq_add_neg, tsub_eq_zero_iff_le.mpr h, pow_zero, mul_one]
  by_cases h0 :
    C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
  · exact (le_of_eq (by simp only [h0, natDegree_zero])).trans_lt hq
  apply lt_of_le_of_ne
  · compute_degree!
    rwa [Nat.sub_add_cancel]
  · contrapose h0
    rw [← leadingCoeff_eq_zero, leadingCoeff, h0, mul_assoc, X_pow_mul, ← tsub_add_cancel_of_le h,
      add_comm _ p.natDegree]
    simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add]
    rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm,
      add_neg_cancel]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)) =
    derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q))

Tactic:
]

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

Goal state before:
pp: case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)

Tactic:
]

Goal state after:
case inr.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      (∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)) =
    ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      (∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q))

Tactic:
]

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

Goal state before:
pp: case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1)) * p.coeff i = a ^ (i - (n + 1)) * p.coeff i

pp: case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ 1 ≤ i - (n + 1)

Tactic:
]

Goal state after:
case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ 1 ≤ i - (n + 1)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ n + 1 + 1 ≤ i

Tactic:
]

Goal state after:
case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ n + 1 + 1 ≤ i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ i ∈ range n.succ, (n + 1).choose (i + 1) • ((⇑derivative)^[n + 1 - (i + 1)] p * (⇑derivative)^[i + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) =
    ∑ k ∈ range n.succ, n.succ.choose (k + 1) • ((⇑derivative)^[n.succ - (k + 1)] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n.succ] p * (⇑derivative)^[0] q)

Tactic:
]

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

Goal state before:
pp: case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ x ∈ range n, n.choose x.succ • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q)

Tactic:
]

Goal state after:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ x ∈ range n, n.choose x.succ • ((⇑derivative)^[n - x] p * (⇑derivative)^[x + 1] q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ (p /ₘ (X - C a)).coeff n = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

Tactic:
]

Goal state after:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)