∀ (f : ℝ ≃ᵐ ℝ) {s : Set ℝ},
  MeasurableSet s →
    ∀ {f' : ℝ → ℝ},
      (∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x) →
        ∀ {g : ℝ → ℝ},
          0 ≤ᵐ[MeasureTheory.volume] g →
            MeasureTheory.Integrable g MeasureTheory.volume →
              (MeasureTheory.Measure.map (⇑f.symm) (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s =
                ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))