simp [hasTemperateGrowth_smul_apply, pow_succ', smul_smul, mul_comm (_ ^ n)]
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) ξ
ξ : ℝ
⊢ (-(2 * ↑π * I)) ^ n •
      -((2 * ↑π * I) •
          𝓕 (fun x => x • ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ξ) =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
no goals