case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n : ℕ
c : R
⊢ (↑derivative^[Nat.zero]) ((X + ↑C c) ^ n) = ↑(∏ i in range Nat.zero, (n - i)) * (X + ↑C c) ^ (n - Nat.zero)

case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n : ℕ
c : R
k : ℕ
IH : (↑derivative^[k]) ((X + ↑C c) ^ n) = ↑(∏ i in range k, (n - i)) * (X + ↑C c) ^ (n - k)
⊢ (↑derivative^[Nat.succ k]) ((X + ↑C c) ^ n) = ↑(∏ i in range (Nat.succ k), (n - i)) * (X + ↑C c) ^ (n - Nat.succ k)
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n k : ℕ
c : R
⊢ (↑derivative^[k]) ((X + ↑C c) ^ n) = ↑(∏ i in range k, (n - i)) * (X + ↑C c) ^ (n - k)
induction' k with k IH
no goals
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n : ℕ
c : R
⊢ (↑derivative^[Nat.zero]) ((X + ↑C c) ^ n) = ↑(∏ i in range Nat.zero, (n - i)) * (X + ↑C c) ^ (n - Nat.zero)
simp
no goals
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n : ℕ
c : R
k : ℕ
IH : (↑derivative^[k]) ((X + ↑C c) ^ n) = ↑(∏ i in range k, (n - i)) * (X + ↑C c) ^ (n - k)
⊢ (↑derivative^[Nat.succ k]) ((X + ↑C c) ^ n) = ↑(∏ i in range (Nat.succ k), (n - i)) * (X + ↑C c) ^ (n - Nat.succ k)
simp only [Function.iterate_succ_apply', IH, derivative_mul, zero_mul, derivative_nat_cast,
  zero_add, Finset.prod_range_succ, C_eq_nat_cast, Nat.sub_sub, ← mul_assoc,
  derivative_X_add_C_pow, Nat.succ_eq_add_one, Nat.cast_mul]