no goals
α : Type u_1
β : Type ?u.11218
γ : Type ?u.11221
δ : Type ?u.11224
ι : Type ?u.11227
R : Type ?u.11230
R' : Type ?u.11233
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
S : Set (Set α)
hs : Set.Countable S
hd : Set.Pairwise S Disjoint
h : ∀ (s : Set α), s ∈ S → MeasurableSet s
⊢ ↑↑μ (⋃₀ S) = ∑' (s : ↑S), ↑↑μ ↑s
rw [sUnion_eq_biUnion, measure_biUnion hs hd h]