no goals
α : Type u_1
β : Type ?u.293051
γ : Type ?u.293054
δ : Type ?u.293057
ι : Type ?u.293060
R : Type ?u.293063
R' : Type ?u.293066
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
hs : MeasurableSet s
⊢ ↑↑(restrict μ univ) s = ↑↑μ s
simp [hs]