∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) (t : Finset ι)
  (p : α → Prop), (∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) = ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x