no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1024019
δ : Type ?u.1024022
m : MeasurableSpace α
μ ν : Measure α
s : Finset β
t : β → Set α
hd : Set.Pairwise (↑s) (AEDisjoint μ on t)
hm : ∀ (b : β), b ∈ s → NullMeasurableSet (t b)
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α) in ⋃ (b : β) (_ : b ∈ s), t b, f a ∂μ) = ∑ b in s, ∫⁻ (a : α) in t b, f a ∂μ
simp only [← Finset.mem_coe, lintegral_biUnion₀ s.countable_toSet hm hd, ← Finset.tsum_subtype']