∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  (K₁ K₂ : TopologicalSpace.Compacts G) {V : Set G},
  (interior V).Nonempty →
    Disjoint (K₁.carrier + -V) (K₂.carrier + -V) →
      MeasureTheory.Measure.haar.addIndex (K₁.carrier ∪ K₂.carrier) V =
        MeasureTheory.Measure.haar.addIndex K₁.carrier V + MeasureTheory.Measure.haar.addIndex K₂.carrier V