no goals
α : Type u_1
β : Type ?u.320231
γ : Type ?u.320234
δ : Type ?u.320237
ι : Type ?u.320240
R : Type ?u.320243
R' : Type ?u.320246
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
S : Set (Set α)
hc : Set.Countable S
hs : ⋃₀ S = univ
⊢ (⋃ (i : Set α) (_ : i ∈ S), i) = univ
rwa [← sUnion_eq_biUnion]