simp only [Real.fourierIntegral_def]
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => deriv (fun y => f y) x) ξ - (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => f x) ξ = 0
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • deriv (fun y => f y) v) -
      (2 * ↑π * I * ↑ξ) • ∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • f v =
    0