no goals
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁴ : IsUnifLocDoublingMeasure μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
E : Type ?u.1198936
inst✝ : NormedAddCommGroup E
S : Set α
K : ℝ
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ S,
    ∀ {ι : Type u_2} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[Ioi 0] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j => ↑↑μ (S ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
filter_upwards [(vitaliFamily μ K).ae_tendsto_measure_inter_div S] with x hx ι l w δ δlim
  xmem using hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)