no goals
α : Type u_1
β : Type u_2
γ : Type ?u.3211462
δ : Type ?u.3211465
ι : Type ?u.3211468
R : Type ?u.3211471
R' : Type ?u.3211474
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ✝ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
μ : MeasureTheory.Measure α
e : α ≃ᵐ β
⊢ Measure.map (↑(symm e)) (Measure.map (↑e) μ) ≪ μ
rw [Measure.map_map, e.symm_comp_self, Measure.map_id] <;> measurability