no goals
α : Type u_1
β : Type ?u.902053
γ : Type ?u.902056
δ : Type ?u.902059
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
⊢ (∫⁻ (a : α), f a + g a ∂μ) = (∫⁻ (a : α), f a ∂μ) + ∫⁻ (a : α), g a ∂μ
rw [lintegral_congr_ae hf.ae_eq_mk, ← lintegral_add_left hf.measurable_mk,
  lintegral_congr_ae (hf.ae_eq_mk.add (ae_eq_refl g))]