∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) {U : Set G},
  (interior U).Nonempty → MeasureTheory.Measure.haar.addPrehaar (↑K₀) U ∈ MeasureTheory.Measure.haar.addHaarProduct ↑K₀