no goals
α : Type u_2
inst✝⁸ : MetricSpace α
inst✝⁷ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝⁶ : IsUnifLocDoublingMeasure μ
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : BorelSpace α
inst✝³ : IsLocallyFiniteMeasure μ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f
K : ℝ
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[Ioi 0] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j => ⨍ (y : α) in closedBall (w j) (δ j), f y ∂μ) l (𝓝 (f x))
filter_upwards [(vitaliFamily μ K).ae_tendsto_average hf] with x hx ι l w δ δlim xmem using
  hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)