no goals
α : Type u_1
β : Type ?u.1534048
γ : Type ?u.1534051
δ : Type ?u.1534054
ι : Type ?u.1534057
R : Type ?u.1534060
R' : Type ?u.1534063
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
hs : MeasurableSet s
p : α → Prop
⊢ (∀ᵐ (x : α) ∂Measure.restrict μ s, p x) ↔ ∀ᵐ (x : ↑s) ∂Measure.comap Subtype.val μ, p ↑x
rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).ae_map_iff]