∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] {s : Set G} [MeasurableInv G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsMulLeftInvariant] [ν'.IsMulLeftInvariant], ν' s ≠ 0 → ν' s ≠ ⊤ → ∀ᵐ (x : G) ∂μ', ν' ((fun y => y * x) ⁻¹' s) < ⊤