-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem coeff_derivative (p : R[X]) (n : ℕ) :
    coeff (derivative p) n = coeff p (n + 1) * (n + 1)

Proof state:
case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ¬p.coeff (n + 1) ≠ 0 → p.coeff (n + 1) * (↑n + 1) = 0

Tactic:
intro h

Result:
case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff (n + 1) ≠ 0
⊢ p.coeff (n + 1) * (↑n + 1) = 0

Proof state:
case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ b ∈ p.support, b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0

Tactic:
intro b

Result:
case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n b : ℕ
⊢ b ∈ p.support → b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff (n + 1) * ↑(n + 1) = p.coeff (n + 1) * (↑n + 1)

Tactic:
norm_cast

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.sum fun a b => b * ↑a * if n = a - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)

Tactic:
rw [sum, Finset.sum_eq_single (n + 1)]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)

case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ b ∈ p.support, b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0

case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ n + 1 ∉ p.support → (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0

Proof state:
case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff (n + 1) ≠ 0
⊢ p.coeff (n + 1) * (↑n + 1) = 0

Tactic:
push_neg at h

Result:
case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff (n + 1) = 0
⊢ p.coeff (n + 1) * (↑n + 1) = 0

Proof state:
case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a✝¹ : 0 ∈ p.support
a✝ : 0 ≠ n + 1
⊢ (p.coeff 0 * ↑0 * if n = 0 - 1 then 1 else 0) = 0

Tactic:
rw [Nat.cast_zero, mul_zero, zero_mul]

Result:
no goals

Proof state:
case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff (n + 1) = 0
⊢ p.coeff (n + 1) * (↑n + 1) = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n b : ℕ
⊢ b ∈ p.support → b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0

Tactic:
cases b

Result:
case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ 0 ∈ p.support → 0 ≠ n + 1 → (p.coeff 0 * ↑0 * if n = 0 - 1 then 1 else 0) = 0

case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ n✝ + 1 ∈ p.support → n✝ + 1 ≠ n + 1 → (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0

Proof state:
case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ 0 ∈ p.support → 0 ≠ n + 1 → (p.coeff 0 * ↑0 * if n = 0 - 1 then 1 else 0) = 0

Tactic:
intros

Result:
case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a✝¹ : 0 ∈ p.support
a✝ : 0 ≠ n + 1
⊢ (p.coeff 0 * ↑0 * if n = 0 - 1 then 1 else 0) = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)

Tactic:
rw [derivative_apply]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.sum fun n a => C (a * ↑n) * X ^ (n - 1)).coeff n = p.coeff (n + 1) * (↑n + 1)

Proof state:
case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ n✝ + 1 ∈ p.support → n✝ + 1 ≠ n + 1 → (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0

Tactic:
intro _ H

Result:
case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : n✝ + 1 ∈ p.support
H : n✝ + 1 ≠ n + 1
⊢ (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.sum fun n a => C (a * ↑n) * X ^ (n - 1)).coeff n = p.coeff (n + 1) * (↑n + 1)

Tactic:
simp only [coeff_X_pow, coeff_sum, coeff_C_mul]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.sum fun a b => b * ↑a * if n = a - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)

Proof state:
case h₀.succ
R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : n✝ + 1 ∈ p.support
H : n✝ + 1 ≠ n + 1
⊢ (p.coeff (n✝ + 1) * ↑(n✝ + 1) * if n = n✝ + 1 - 1 then 1 else 0) = 0

Tactic:
rw [Nat.add_one_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)

Tactic:
simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true, eq_self_iff_true]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff (n + 1) * ↑(n + 1) = p.coeff (n + 1) * (↑n + 1)

Proof state:
case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ n + 1 ∉ p.support → (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0

Tactic:
rw [if_pos (add_tsub_cancel_right n 1).symm, mul_one, Nat.cast_add, Nat.cast_one,
  mem_support_iff]

Result:
case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ¬p.coeff (n + 1) ≠ 0 → p.coeff (n + 1) * (↑n + 1) = 0