∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (K₁ K₂ : TopologicalSpace.Compacts G),
  Disjoint ↑K₁ ↑K₂ →
    IsClosed ↑K₂ →
      ⟨MeasureTheory.Measure.haar.chaar K₀ (K₁ ⊔ K₂), ⋯⟩ =
        ⟨MeasureTheory.Measure.haar.chaar K₀ K₁, ⋯⟩ + ⟨MeasureTheory.Measure.haar.chaar K₀ K₂, ⋯⟩