simp
case zero
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
⊢ (iteratedDeriv Nat.zero fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ Nat.zero),
      Nat.choose Nat.zero i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.zero - i) (⇑f) x
no goals