induction n generalizing ξ with
| zero => simp
| succ n IH =>
  rw [iteratedDeriv_succ]
  conv => lhs; arg 1; intro ζ
  simp only [IH, ← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_pow n)]
  rw [deriv_const_smul _ (differentiable_fourierIntegral _ ξ), deriv_fourierIntegral]
  simp [hasTemperateGrowth_smul_apply, pow_succ', smul_smul, mul_comm (_ ^ n)]
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ iteratedDeriv n (fun ξ => 𝓕 (fun x => f x) ξ) ξ = (-(2 * ↑π * I)) ^ n • 𝓕 (fun x => x ^ n • f x) ξ
no goals