Theorem: SchwartzMap.Real.fourierIntegral_sub (ForML/SchwartzRealFourier.lean)

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => f x - g x) ξ = 𝓕 (fun x => f x) ξ - 𝓕 (fun x => g x) ξ
Tactic:
simpa [Real.fourierIntegral_def, smul_sub] using
  integral_sub (integrable_fourierIntegrand f ξ) (integrable_fourierIntegrand g ξ)
State after:
no goals