simp only [← iteratedDeriv_eq_iteratedPDeriv]
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => ((iteratedPDeriv ℝ fun x => 1) f) x) ξ =
    (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
n : ℕ
IH : 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
⊢ (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => iteratedDeriv n (⇑f) x) ξ = (2 * ↑π * I * ↑ξ) ^ Nat.succ n • 𝓕 (fun y => f y) ξ