rw [F_add]
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x + -g x) x = 𝓕 f x + -𝓕 g x
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x) x + 𝓕 (fun x => -g x) x = 𝓕 f x + -𝓕 g x

case hf
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => f x) volume

case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume