case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ degree (↑derivative p) ≤ ↑(natDegree p - 1)

case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ↑(natDegree p - 1) ≤ degree (↑derivative p)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ degree (↑derivative p) = ↑(natDegree p - 1)
apply le_antisymm
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ degree (sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) ≤ ↑(natDegree p - 1)
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ degree (↑derivative p) ≤ ↑(natDegree p - 1)
rw [derivative_apply]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ∀ (b : ℕ), b ∈ support p → degree ((fun n a => ↑C (a * ↑n) * X ^ (n - 1)) b (coeff p b)) ≤ ↑(natDegree p - 1)
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ degree (sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) ≤ ↑(natDegree p - 1)
apply le_trans (degree_sum_le _ _) (Finset.sup_le _)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
n : ℕ
hn : n ∈ support p
⊢ degree ((fun n a => ↑C (a * ↑n) * X ^ (n - 1)) n (coeff p n)) ≤ ↑(natDegree p - 1)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ∀ (b : ℕ), b ∈ support p → degree ((fun n a => ↑C (a * ↑n) * X ^ (n - 1)) b (coeff p b)) ≤ ↑(natDegree p - 1)
intro n hn
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
n : ℕ
hn : n ∈ support p
⊢ degree (↑C (coeff p n * ↑n) * X ^ (n - 1)) ≤ ↑(natDegree p - 1)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
n : ℕ
hn : n ∈ support p
⊢ degree ((fun n a => ↑C (a * ↑n) * X ^ (n - 1)) n (coeff p n)) ≤ ↑(natDegree p - 1)
simp only [Nat.cast_withBot]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
n : ℕ
hn : n ∈ support p
⊢ n ≤ natDegree p
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
n : ℕ
hn : n ∈ support p
⊢ degree (↑C (coeff p n * ↑n) * X ^ (n - 1)) ≤ ↑(natDegree p - 1)
apply le_trans (degree_C_mul_X_pow_le _ _) (WithBot.coe_le_coe.2 (tsub_le_tsub_right _ _))
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
n : ℕ
hn : n ∈ support p
⊢ n ≤ natDegree p
apply le_natDegree_of_mem_supp _ hn
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ natDegree p - 1 ∈ support (↑derivative p)
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ↑(natDegree p - 1) ≤ degree (↑derivative p)
refine' le_sup _
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ coeff p (natDegree p) ≠ 0

case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ 1 ≤ natDegree p
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ natDegree p - 1 ∈ support (↑derivative p)
rw [mem_support_derivative, tsub_add_cancel_of_le, mem_support_iff]
no goals
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ 1 ≤ natDegree p
exact hp
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ¬leadingCoeff p = 0
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ coeff p (natDegree p) ≠ 0
show ¬leadingCoeff p = 0
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ¬p = 0
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ¬leadingCoeff p = 0
rw [leadingCoeff_eq_zero]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
h : p = 0
⊢ False
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
⊢ ¬p = 0
intro h
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < 0
h : p = 0
⊢ False
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < natDegree p
h : p = 0
⊢ False
rw [h, natDegree_zero] at hp
no goals
case a
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < 0
h : p = 0
⊢ False
exact lt_irrefl 0 (lt_of_le_of_lt (zero_le _) hp)