no goals
α : Type u_1
β : Type u_2
γ : Type ?u.2593974
δ : Type ?u.2593977
ι : Type ?u.2593980
R : Type ?u.2593983
R' : Type ?u.2593986
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
e : α ≃ᵐ β
⊢ Measure.map (↑e) μ = ν ↔ Measure.map (↑(symm e)) ν = μ
rw [← (map_measurableEquiv_injective e).eq_iff, map_map_symm, eq_comm]