∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) →
    (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
      ∀ {t : Set α}, MeasurableSet t → (μ.restrict (⋃ i, s i)) t = ∑' (i : ι), (μ.restrict (s i)) t