induction n with
| zero => simp
| succ n IH =>
  rw [iteratedDeriv_succ]
  conv => lhs; arg 1; intro x; arg 1; intro z
  simp only [iteratedDeriv_eq_iteratedPDeriv]
  rw [fourierIntegral_deriv]
  simp only [← iteratedDeriv_eq_iteratedPDeriv]
  rw [IH]
  simp [pow_succ, smul_smul]
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => iteratedDeriv n (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) ^ n • 𝓕 (fun x => f x) ξ
no goals