-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_eq_zero {p : R[X]} {x : ℕ} (hx : p.natDegree < x) :
    Polynomial.derivative^[x] p = 0

Proof state:
case h
R : Type u
inst✝ : Semiring R
n✝ : ℕ
ih : ∀ m < n✝, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
p : R[X]
x : ℕ
hx : p.natDegree < x
h : p.natDegree = n✝
⊢ (⇑derivative)^[x] p = 0

Tactic:
subst h

Result:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
⊢ (⇑derivative)^[x] p = 0

Proof state:
case h.intro
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ (⇑derivative)^[t.succ] p = 0

Tactic:
rw [Function.iterate_succ_apply]

Result:
case h.intro
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ (⇑derivative)^[t] (derivative p) = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
⊢ (⇑derivative)^[x] p = 0

Tactic:
induction' h : p.natDegree using Nat.strong_induction_on with _ ih generalizing p x

Result:
case h
R : Type u
inst✝ : Semiring R
n✝ : ℕ
ih : ∀ m < n✝, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
p : R[X]
x : ℕ
hx : p.natDegree < x
h : p.natDegree = n✝
⊢ (⇑derivative)^[x] p = 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0

Tactic:
rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]

Result:
no goals

Proof state:
case h.intro
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ (⇑derivative)^[t] (derivative p) = 0

Tactic:
by_cases hp : p.natDegree = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0

Proof state:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
⊢ (⇑derivative)^[x] p = 0

Tactic:
obtain ⟨t, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne'

Result:
case h.intro
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ (⇑derivative)^[t.succ] p = 0

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
this : (derivative p).natDegree < p.natDegree
⊢ (⇑derivative)^[t] (derivative p) = 0

Tactic:
exact ih _ this (this.trans_le <| Nat.le_of_lt_succ hx) rfl

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0

Tactic:
have := natDegree_derivative_lt hp

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
this : (derivative p).natDegree < p.natDegree
⊢ (⇑derivative)^[t] (derivative p) = 0