rw [iteratedDeriv_succ]
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ iteratedDeriv (Nat.succ n) (fun ξ => 𝓕 (fun x => f x) ξ) ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
n : ℕ
IH : ∀ {ξ : ℝ}, iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
ξ : ℝ
⊢ deriv (iteratedDeriv n fun ξ => 𝓕 (fun x => f x) ξ) ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ