no goals
α : Type u_1
β : Type u_2
γ : Type ?u.2129036
δ : Type ?u.2129039
ι : Type ?u.2129042
R : Type ?u.2129045
R' : Type ?u.2129048
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
e : α ≃ᵐ β
⊢ Measure.map (↑(symm e)) (Measure.map (↑e) μ) = μ
simp [map_map e.symm.measurable e.measurable]