∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (K₀ : TopologicalSpace.PositiveCompacts G)
  {U : Set G} (K : TopologicalSpace.Compacts G), 0 ≤ MeasureTheory.Measure.haar.addPrehaar (↑K₀) U K