∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G},
  μ.IsEverywherePos k → IsCompact k → IsClosed k → IsGδ k