rw [deriv_const_smul _ (differentiable_fourierIntegral _ ξ), deriv_fourierIntegral]
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) ξ
ξ : ℝ
⊢ deriv
      (fun ζ =>
        (-(2 * ↑π * I)) ^ n •
          𝓕 (fun x => ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ n)) f) x) ζ)
      ξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • 𝓕 (fun x => x ^ Nat.succ n • f x) ξ
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) ξ