no goals
ι : Type ?u.3617330
α : Type u_1
β : Type u_2
γ : Type ?u.3617339
δ : Type ?u.3617342
R : Type ?u.3617345
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g : α → β
μ✝ ν : MeasureTheory.Measure α
s : Set α
hs : MeasurableSet s
μ : MeasureTheory.Measure α
f : α → β
⊢ AEMeasurable f ↔ AEMeasurable (f ∘ Subtype.val)
rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).aemeasurable_map_iff]