simp [Real.fourierIntegral_def, integral_neg,
  ← smul_smul (2 * π * I), smul_comm _ (2 * π * I), integral_smul]
case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) ξ = -((2 * ↑π * I) • 𝓕 (fun x => x • f x) ξ)
no goals