∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant]
  [ν.IsMulLeftInvariant],
  MeasurableSet s →
    ∀ (f : G → ENNReal), Measurable f → μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ