no goals
α : Type u_1
β : Type ?u.291299
γ : Type ?u.291302
δ : Type ?u.291305
ι : Type ?u.291308
R : Type ?u.291311
R' : Type ?u.291314
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ s) t = 0 ↔ ↑↑μ (t ∩ s) = 0
rw [restrict_apply ht]