no goals
α : Type u_1
β : Type ?u.1576020
γ : Type ?u.1576023
δ : Type ?u.1576026
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f✝ g✝ : α →ₘ[μ] ℝ≥0∞
f : α → ℝ≥0∞
hf : AEStronglyMeasurable f μ
g : α → ℝ≥0∞
x✝ : AEStronglyMeasurable g μ
⊢ lintegral (mk f hf + mk g x✝) = lintegral (mk f hf) + lintegral (mk g x✝)
simp [lintegral_add_left' hf.aemeasurable]