case inl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p = 0
⊢ natDegree (↑derivative p) < natDegree p

case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p ≠ 0
⊢ natDegree (↑derivative p) < natDegree p
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
⊢ natDegree (↑derivative p) < natDegree p
cases' eq_or_ne (derivative p) 0 with hp' hp'
case inl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p = 0
⊢ 0 < natDegree p
case inl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p = 0
⊢ natDegree (↑derivative p) < natDegree p
rw [hp', Polynomial.natDegree_zero]
no goals
case inl
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p = 0
⊢ 0 < natDegree p
exact hp.bot_lt
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p ≠ 0
⊢ degree (↑derivative p) < degree p
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p ≠ 0
⊢ natDegree (↑derivative p) < natDegree p
rw [natDegree_lt_natDegree_iff hp']
no goals
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p ≠ 0
hp' : ↑derivative p ≠ 0
⊢ degree (↑derivative p) < degree p
exact degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)