{G : Type w} →
  [inst : TopologicalSpace G] →
    {motive : MeasureTheory.Content G → Sort u} →
      (t : MeasureTheory.Content G) →
        ((toFun : TopologicalSpace.Compacts G → NNReal) →
            (mono' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), ↑K₁ ⊆ ↑K₂ → toFun K₁ ≤ toFun K₂) →
              (sup_disjoint' :
                  ∀ (K₁ K₂ : TopologicalSpace.Compacts G),
                    Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → toFun (K₁ ⊔ K₂) = toFun K₁ + toFun K₂) →
                (sup_le' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), toFun (K₁ ⊔ K₂) ≤ toFun K₁ + toFun K₂) →
                  motive { toFun := toFun, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' }) →
          motive t