no goals
ι : Type ?u.12882374
𝕜 : Type ?u.12882377
E : Type u_1
F : Type ?u.12882383
A : Type ?u.12882386
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
⊢ (∫ (x : ℝ) in a..b, f x - g x ∂μ) = (∫ (x : ℝ) in a..b, f x ∂μ) - ∫ (x : ℝ) in a..b, g x ∂μ
simpa only [sub_eq_add_neg] using (integral_add hf hg.neg).trans (congr_arg _ integral_neg)