no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1189
δ : Type ?u.1192
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa✝ : Measure α
μb✝ : Measure β
μc : Measure γ
μd : Measure δ
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving ↑e
⊢ map (↑(MeasurableEquiv.symm e)) μb = μa
rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]