case zero
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n : ℕ
⊢ (↑derivative^[Nat.zero]) (X ^ n) = ↑(Nat.descFactorial n Nat.zero) * X ^ (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 k : ℕ
ih : (↑derivative^[k]) (X ^ n) = ↑(Nat.descFactorial n k) * X ^ (n - k)
⊢ (↑derivative^[Nat.succ k]) (X ^ n) = ↑(Nat.descFactorial n (Nat.succ k)) * X ^ (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 : ℕ
⊢ (↑derivative^[k]) (X ^ n) = ↑(Nat.descFactorial n k) * X ^ (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 : ℕ
⊢ (↑derivative^[Nat.zero]) (X ^ n) = ↑(Nat.descFactorial n Nat.zero) * X ^ (n - Nat.zero)
erw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n k : ℕ
ih : (↑derivative^[k]) (X ^ n) = ↑(Nat.descFactorial n k) * X ^ (n - k)
⊢ ↑(Nat.descFactorial n k) * (↑(n - k) * X ^ (n - (k + 1))) = ↑(n - k) * ↑(Nat.descFactorial n k) * X ^ (n - (k + 1))
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
n k : ℕ
ih : (↑derivative^[k]) (X ^ n) = ↑(Nat.descFactorial n k) * X ^ (n - k)
⊢ (↑derivative^[Nat.succ k]) (X ^ n) = ↑(Nat.descFactorial n (Nat.succ k)) * X ^ (n - Nat.succ k)
rw [Function.iterate_succ_apply', ih, derivative_nat_cast_mul, derivative_X_pow, C_eq_nat_cast,
  Nat.succ_eq_add_one, Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
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 k : ℕ
ih : (↑derivative^[k]) (X ^ n) = ↑(Nat.descFactorial n k) * X ^ (n - k)
⊢ ↑(Nat.descFactorial n k) * (↑(n - k) * X ^ (n - (k + 1))) = ↑(n - k) * ↑(Nat.descFactorial n k) * X ^ (n - (k + 1))
simp [mul_comm, mul_assoc, mul_left_comm]