no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.53763
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
f : α → β
hf : MeasurePreserving f
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEMeasurable (g ∘ f) ↔ AEMeasurable g
rw [← hf.map_eq, h₂.aemeasurable_map_iff]