∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : MeasurableSpace β]
  (g : MeasureTheory.SimpleFunc β ENNReal) {f : α → β} (hf : Measurable f),
  g.lintegral (MeasureTheory.Measure.map f μ) = (g.comp f hf).lintegral μ