no goals
α : Type u_1
β : Type ?u.291960
γ : Type ?u.291963
δ : Type ?u.291966
ι : Type ?u.291969
R : Type ?u.291972
R' : Type ?u.291975
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : MeasurableSet s
⊢ ↑↑(restrict μ s) t = 0 ↔ ↑↑μ (t ∩ s) = 0
rw [restrict_apply' hs]