∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] [inst_3 : Group G]
  [IsTopologicalGroup G] [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : MeasureTheory.Measure G)
  [μ.IsOpenPosMeasure] [μ.IsMulLeftInvariant], μ Set.univ = ⊤