no goals
α : Type u_2
β✝ : Type ?u.393825
γ : Type u_3
ι : Type ?u.393831
inst✝² : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β✝
inst✝ : TopologicalSpace γ
f✝ g✝ : α → β✝
β : Type u_1
f : α → β
mα : MeasurableSpace α
μa : Measure α
mβ : MeasurableSpace β
μb : Measure β
hf : MeasurePreserving f
h₂ : MeasurableEmbedding f
g : β → γ
⊢ AEStronglyMeasurable (g ∘ f) μa ↔ AEStronglyMeasurable g μb
rw [← hf.map_eq, h₂.aestronglyMeasurable_map_iff]