∀ {α : Type u_1} {C : Set (Set α)} (m : MeasureTheory.AddContent ENNReal C) (I : Finset (Set α)),
  ↑I ⊆ C →
    (↑I).PairwiseDisjoint id →
      ⋃₀ ↑I ∈ C → MeasureTheory.extend (fun x x_1 => m x) (⋃₀ ↑I) = ∑ u ∈ I, MeasureTheory.extend (fun x x_1 => m x) u