∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) {K : Set G} (h1K : IsCompact K)
  (h2K : IsOpen K), μ.innerContent { carrier := K, is_open' := h2K } = μ { carrier := K, isCompact' := h1K }