∀ {G : Type u_3} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G},
  (∀ ⦃K : Set G⦄, IsCompact K → μ K < ⊤) →
    (∀ (g : G), MeasureTheory.Measure.map (fun x => g * x) μ = μ) →
      (∀ (U : Set G), IsOpen U → U.Nonempty → μ U ≠ 0) → μ.IsHaarMeasure