∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSpace β]
  {f : α → β}, Measurable f → ∀ {s : Set β}, MeasurableSet s → (MeasureTheory.Measure.map f μ).real s = μ.real (f ⁻¹' s)