no goals
α : Type u_1
β : Type u_2
γ : Type ?u.2284080
δ : Type ?u.2284083
ι : Type ?u.2284086
R : Type ?u.2284089
R' : Type ?u.2284092
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
e : α ≃ᵐ β
⊢ Measure.map (↑e) (Measure.map (↑(symm e)) ν) = ν
simp [map_map e.measurable e.symm.measurable]