no goals
α : Type u_1
β : Type ?u.726384
γ : Type ?u.726387
δ : Type ?u.726390
ι : Type ?u.726393
R : Type ?u.726396
R' : Type ?u.726399
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ (⋃ (i : ℕ), spanningSets μ i) = univ
simp_rw [spanningSets, iUnion_accumulate, μ.toFiniteSpanningSetsIn.spanning]