case h
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x✝¹ : ℕ
hx✝ : natDegree p✝ < x✝¹
x✝ : ℕ
h✝ : natDegree p✝ = x✝
n✝ : ℕ
ih : ∀ (m : ℕ), m < n✝ → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
p : R[X]
x : ℕ
hx : natDegree p < x
h : natDegree p = n✝
⊢ (↑derivative^[x]) p = 0
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
x : ℕ
hx : natDegree p < x
⊢ (↑derivative^[x]) p = 0
induction' h : p.natDegree using Nat.strong_induction_on with _ ih generalizing p x
case h
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x✝¹ : ℕ
hx✝ : natDegree p✝ < x✝¹
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
x : ℕ
hx : natDegree p < x
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
⊢ (↑derivative^[x]) p = 0
case h
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x✝¹ : ℕ
hx✝ : natDegree p✝ < x✝¹
x✝ : ℕ
h✝ : natDegree p✝ = x✝
n✝ : ℕ
ih : ∀ (m : ℕ), m < n✝ → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
p : R[X]
x : ℕ
hx : natDegree p < x
h : natDegree p = n✝
⊢ (↑derivative^[x]) p = 0
subst h
case h.intro
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
t : ℕ
hx : natDegree p < Nat.succ t
⊢ (↑derivative^[Nat.succ t]) p = 0
case h
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x✝¹ : ℕ
hx✝ : natDegree p✝ < x✝¹
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
x : ℕ
hx : natDegree p < x
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
⊢ (↑derivative^[x]) p = 0
obtain ⟨t, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne'
case h.intro
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
t : ℕ
hx : natDegree p < Nat.succ t
⊢ (↑derivative^[t]) (↑derivative p) = 0
case h.intro
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
t : ℕ
hx : natDegree p < Nat.succ t
⊢ (↑derivative^[Nat.succ t]) p = 0
rw [Function.iterate_succ_apply]
case pos
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
t : ℕ
hx : natDegree p < Nat.succ t
hp : natDegree p = 0
⊢ (↑derivative^[t]) (↑derivative p) = 0

case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
t : ℕ
hx : natDegree p < Nat.succ t
hp : ¬natDegree p = 0
⊢ (↑derivative^[t]) (↑derivative p) = 0
case h.intro
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
t : ℕ
hx : natDegree p < Nat.succ t
⊢ (↑derivative^[t]) (↑derivative p) = 0
by_cases hp : p.natDegree = 0
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
t : ℕ
hx : natDegree p < Nat.succ t
hp : ¬natDegree p = 0
this : natDegree (↑derivative p) < natDegree p
⊢ (↑derivative^[t]) (↑derivative p) = 0
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
t : ℕ
hx : natDegree p < Nat.succ t
hp : ¬natDegree p = 0
⊢ (↑derivative^[t]) (↑derivative p) = 0
have := natDegree_derivative_lt hp
no goals
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
t : ℕ
hx : natDegree p < Nat.succ t
hp : ¬natDegree p = 0
this : natDegree (↑derivative p) < natDegree p
⊢ (↑derivative^[t]) (↑derivative p) = 0
exact ih _ this (this.trans_le <| Nat.le_of_lt_succ hx) rfl
no goals
case pos
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ : R[X]
x : ℕ
hx✝ : natDegree p✝ < x
x✝ : ℕ
h : natDegree p✝ = x✝
p : R[X]
ih : ∀ (m : ℕ), m < natDegree p → ∀ {p : R[X]} {x : ℕ}, natDegree p < x → natDegree p = m → (↑derivative^[x]) p = 0
t : ℕ
hx : natDegree p < Nat.succ t
hp : natDegree p = 0
⊢ (↑derivative^[t]) (↑derivative p) = 0
rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]