no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1020799
δ : Type ?u.1020802
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
s : β → Set α
hm : ∀ (i : β), NullMeasurableSet (s i)
hd : Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α) in ⋃ (i : β), s i, f a ∂μ) = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
simp only [Measure.restrict_iUnion_ae hd hm, lintegral_sum_measure]