induction n using ENat.nat_induction generalizing f with
| h0 => simpa [contDiff_zero] using continuous_fourierIntegral f
| hsuc n IH =>
  rw [contDiff_succ_iff_deriv]
  refine And.intro (differentiable_fourierIntegral f) ?_
  conv => arg 3; intro ξ
  simp only [deriv_fourierIntegral]
  refine ContDiff.neg ?_
  refine ContDiff.const_smul _ ?_
  simp only [← hasTemperateGrowth_smul_apply (Function.hasTemperateGrowth_id')]
  exact IH _
| htop IH => exact contDiff_top.mpr fun n ↦ IH n f
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ∞
f : 𝓢(ℝ, F)
⊢ ContDiff ℝ n fun ξ => 𝓕 (fun x => f x) ξ
no goals