no goals
α : Type u_1
β : Type ?u.731158
γ : Type ?u.731161
δ : Type ?u.731164
ι : Type ?u.731167
R : Type ?u.731170
R' : Type ?u.731173
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : SigmaFinite μ
hs : MeasurableSet s
⊢ ↑↑(restrict μ (⋃ (i : ℕ), spanningSets μ i)) s = ↑↑μ s
rw [iUnion_spanningSets, restrict_univ]