-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem degree_derivative_eq [NoZeroSMulDivisors ℕ R] (p : R[X]) (hp : 0 < natDegree p) :
    degree (derivative p) = (natDegree p - 1 : ℕ)

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
n : ℕ
hn : n ∈ p.support
⊢ n ≤ p.natDegree

Tactic:
apply le_natDegree_of_mem_supp _ hn

Result:
no goals

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ (p.sum fun n a => C (a * ↑n) * X ^ (n - 1)).degree ≤ ↑(p.natDegree - 1)

Tactic:
apply le_trans (degree_sum_le _ _) (Finset.sup_le _)

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ ∀ b ∈ p.support, ((fun n a => C (a * ↑n) * X ^ (n - 1)) b (p.coeff b)).degree ≤ ↑(p.natDegree - 1)

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
n : ℕ
hn : n ∈ p.support
⊢ ((fun n a => C (a * ↑n) * X ^ (n - 1)) n (p.coeff n)).degree ≤ ↑(p.natDegree - 1)

Tactic:
apply le_trans (degree_C_mul_X_pow_le _ _) (WithBot.coe_le_coe.2 (tsub_le_tsub_right _ _))

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
n : ℕ
hn : n ∈ p.support
⊢ n ≤ p.natDegree

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ ¬p = 0

Tactic:
intro h

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
h : p = 0
⊢ False

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ p.natDegree - 1 ∈ (derivative p).support

Tactic:
rw [mem_support_derivative, tsub_add_cancel_of_le, mem_support_iff]

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ p.coeff p.natDegree ≠ 0

case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ 1 ≤ p.natDegree

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ 1 ≤ p.natDegree

Tactic:
exact hp

Result:
no goals

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
h : p = 0
⊢ False

Tactic:
rw [h, natDegree_zero] at hp

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < 0
h : p = 0
⊢ False

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ ↑(p.natDegree - 1) ≤ (derivative p).degree

Tactic:
refine le_sup ?_

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ p.natDegree - 1 ∈ (derivative p).support

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < 0
h : p = 0
⊢ False

Tactic:
exact hp.false

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ (derivative p).degree = ↑(p.natDegree - 1)

Tactic:
apply le_antisymm

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ (derivative p).degree ≤ ↑(p.natDegree - 1)

case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ ↑(p.natDegree - 1) ≤ (derivative p).degree

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ (derivative p).degree ≤ ↑(p.natDegree - 1)

Tactic:
rw [derivative_apply]

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ (p.sum fun n a => C (a * ↑n) * X ^ (n - 1)).degree ≤ ↑(p.natDegree - 1)

Proof state:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ p.coeff p.natDegree ≠ 0

Tactic:
rw [coeff_natDegree, Ne, leadingCoeff_eq_zero]

Result:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ ¬p = 0

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
⊢ ∀ b ∈ p.support, ((fun n a => C (a * ↑n) * X ^ (n - 1)) b (p.coeff b)).degree ≤ ↑(p.natDegree - 1)

Tactic:
intro n hn

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
hp : 0 < p.natDegree
n : ℕ
hn : n ∈ p.support
⊢ ((fun n a => C (a * ↑n) * X ^ (n - 1)) n (p.coeff n)).degree ≤ ↑(p.natDegree - 1)