∀ {ι : Type u_1} {α : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsFiniteMeasure μ] {r : ENNReal} [Infinite ι] {s : ι → Set α},
  (∀ (i : ι), MeasurableSet (s i)) →
    r ≠ 0 → (∀ (i : ι), r ≤ μ (s i)) → ∃ t, t.Infinite ∧ ∀ ⦃u : Set ι⦄, u ⊆ t → u.Finite → 0 < μ (⋂ i ∈ u, s i)