no goals
α : Type u_1
β : Type ?u.285491
γ : Type ?u.285494
δ : Type ?u.285497
ι : Type ?u.285500
R : Type ?u.285503
R' : Type ?u.285506
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
⊢ ↑↑(restrict μ s) univ = ↑↑μ s
rw [restrict_apply MeasurableSet.univ, Set.univ_inter]