no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ ↑derivative (p ^ (Nat.zero + 1)) = ↑C (↑Nat.zero + 1) * p ^ Nat.zero * ↑derivative p
simp
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : ↑derivative (p ^ (n + 1)) = ↑C (↑n + 1) * p ^ n * ↑derivative p
⊢ (↑C ↑n * p ^ n * p + p ^ n * p) * ↑derivative p + p ^ n * p * ↑derivative p =
    ↑C (↑(Nat.succ n) + 1) * p ^ n * p * ↑derivative p
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : ↑derivative (p ^ (n + 1)) = ↑C (↑n + 1) * p ^ n * ↑derivative p
⊢ ↑derivative (p ^ (Nat.succ n + 1)) = ↑C (↑(Nat.succ n) + 1) * p ^ Nat.succ n * ↑derivative p
rw [pow_succ', derivative_mul, ih, Nat.add_one, mul_right_comm, C_add,
  add_mul, add_mul, pow_succ', ← mul_assoc, C_1, one_mul]
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : ↑derivative (p ^ (n + 1)) = ↑C (↑n + 1) * p ^ n * ↑derivative p
⊢ (↑C ↑n * p ^ n * p + p ^ n * p) * ↑derivative p + p ^ n * p * ↑derivative p =
    ↑C (↑(Nat.succ n) + 1) * p ^ n * p * ↑derivative p
simp [add_mul]