∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (K₀ : TopologicalSpace.PositiveCompacts G),
  MeasureTheory.Measure.addHaarMeasure K₀ =
    ((MeasureTheory.Measure.haar.addHaarContent K₀).measure ↑K₀)⁻¹ •
      (MeasureTheory.Measure.haar.addHaarContent K₀).measure