no goals
α : Type u_2
β✝ : Type ?u.579235
γ : Type ?u.579238
δ : Type ?u.579241
ι : Type ?u.579244
R : Type ?u.579247
R' : Type ?u.579250
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β✝
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
⊢ t ∈ Filter.map f (ae (Measure.restrict μ s)) ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
rw [mem_map, mem_ae_iff, Measure.restrict_apply' hs]