R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ coeff (sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) n = coeff p (n + 1) * (↑n + 1)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ coeff (↑derivative p) n = coeff p (n + 1) * (↑n + 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
p : R[X]
n : ℕ
⊢ (sum p fun a b => b * ↑a * if n = a - 1 then 1 else 0) = coeff p (n + 1) * (↑n + 1)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ coeff (sum p fun n a => ↑C (a * ↑n) * X ^ (n - 1)) n = coeff p (n + 1) * (↑n + 1)
simp only [coeff_X_pow, coeff_sum, coeff_C_mul]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = coeff p (n + 1) * (↑n + 1)

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]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 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]
n : ℕ
⊢ ¬n + 1 ∈ support p → (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 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]
n : ℕ
⊢ (sum p fun a b => b * ↑a * if n = a - 1 then 1 else 0) = coeff p (n + 1) * (↑n + 1)
rw [sum, Finset.sum_eq_single (n + 1)]
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ coeff p (n + 1) * ↑(n + 1) = coeff p (n + 1) * (↑n + 1)

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]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 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]
n : ℕ
⊢ ¬n + 1 ∈ support p → (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 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]
n : ℕ
⊢ (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = coeff p (n + 1) * (↑n + 1)

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]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 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]
n : ℕ
⊢ ¬n + 1 ∈ support p → (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0
simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true, eq_self_iff_true]
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]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 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]
n : ℕ
⊢ ¬n + 1 ∈ support p → (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 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]
n : ℕ
⊢ coeff p (n + 1) * ↑(n + 1) = coeff p (n + 1) * (↑n + 1)

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]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 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]
n : ℕ
⊢ ¬n + 1 ∈ support p → (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0
norm_cast
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]
n b : ℕ
⊢ b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 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]
n : ℕ
⊢ ∀ (b : ℕ), b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 0
intro b
case h₀.zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ Nat.zero ∈ support p → Nat.zero ≠ n + 1 → (coeff p Nat.zero * ↑Nat.zero * if n = Nat.zero - 1 then 1 else 0) = 0

case h₀.succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ Nat.succ n✝ ∈ support p →
    Nat.succ n✝ ≠ n + 1 → (coeff p (Nat.succ n✝) * ↑(Nat.succ n✝) * if n = Nat.succ n✝ - 1 then 1 else 0) = 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]
n b : ℕ
⊢ b ∈ support p → b ≠ n + 1 → (coeff p b * ↑b * if n = b - 1 then 1 else 0) = 0
cases b
case h₀.zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
a✝¹ : Nat.zero ∈ support p
a✝ : Nat.zero ≠ n + 1
⊢ (coeff p Nat.zero * ↑Nat.zero * if n = Nat.zero - 1 then 1 else 0) = 0
case h₀.zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ Nat.zero ∈ support p → Nat.zero ≠ n + 1 → (coeff p Nat.zero * ↑Nat.zero * if n = Nat.zero - 1 then 1 else 0) = 0
intros
no goals
case h₀.zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
a✝¹ : Nat.zero ∈ support p
a✝ : Nat.zero ≠ n + 1
⊢ (coeff p Nat.zero * ↑Nat.zero * if n = Nat.zero - 1 then 1 else 0) = 0
rw [Nat.cast_zero, mul_zero, zero_mul]
case h₀.succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : Nat.succ n✝ ∈ support p
H : Nat.succ n✝ ≠ n + 1
⊢ (coeff p (Nat.succ n✝) * ↑(Nat.succ n✝) * if n = Nat.succ n✝ - 1 then 1 else 0) = 0
case h₀.succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ Nat.succ n✝ ∈ support p →
    Nat.succ n✝ ≠ n + 1 → (coeff p (Nat.succ n✝) * ↑(Nat.succ n✝) * if n = Nat.succ n✝ - 1 then 1 else 0) = 0
intro _ H
no goals
case h₀.succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
a✝ : Nat.succ n✝ ∈ support p
H : Nat.succ n✝ ≠ n + 1
⊢ (coeff p (Nat.succ n✝) * ↑(Nat.succ n✝) * if n = Nat.succ n✝ - 1 then 1 else 0) = 0
rw [Nat.succ_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]
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]
n : ℕ
⊢ ¬coeff p (n + 1) ≠ 0 → coeff p (n + 1) * (↑n + 1) = 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]
n : ℕ
⊢ ¬n + 1 ∈ support p → (coeff p (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0
rw [if_pos (add_tsub_cancel_right n 1).symm, mul_one, Nat.cast_add, Nat.cast_one,
  mem_support_iff]
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]
n : ℕ
h : ¬coeff p (n + 1) ≠ 0
⊢ coeff p (n + 1) * (↑n + 1) = 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]
n : ℕ
⊢ ¬coeff p (n + 1) ≠ 0 → coeff p (n + 1) * (↑n + 1) = 0
intro h
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]
n : ℕ
h : coeff p (n + 1) = 0
⊢ coeff p (n + 1) * (↑n + 1) = 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]
n : ℕ
h : ¬coeff p (n + 1) ≠ 0
⊢ coeff p (n + 1) * (↑n + 1) = 0
push_neg  at h
no goals
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]
n : ℕ
h : coeff p (n + 1) = 0
⊢ coeff p (n + 1) * (↑n + 1) = 0
simp [h]