∀ {α : Type u_1} [inst : MetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ]
  [μ.OuterRegular] {ε : ENNReal},
  ε ≠ 0 →
    ∀ (f : α → Set ℝ) (s : Set α),
      (∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
        ∃ t r,
          t.Countable ∧
            t ⊆ s ∧
              (∀ x ∈ t, r x ∈ f x) ∧
                s ⊆ ⋃ x ∈ t, Metric.closedBall x (r x) ∧ ∑' (x : ↑t), μ (Metric.closedBall (↑x) (r ↑x)) ≤ μ s + ε