no goals
α : Type u_1
β : Type ?u.903143
γ : Type ?u.903146
δ : Type ?u.903149
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g
⊢ (∫⁻ (a : α), f a + g a ∂μ) = (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
simpa only [add_comm] using lintegral_add_left' hg f