∀ {X : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] [inst_4 : TopologicalSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {x : X} {f : X → E},
  ContinuousAt f x →
    StronglyMeasurableAtFilter f (nhds x) μ →
      ∀ {s : ι → Set X} {li : Filter ι},
        Filter.Tendsto s li (nhds x).smallSets →
          ∀ (m : optParam (ι → ℝ) fun i => μ.real (s i)),
            autoParam ((fun i => μ.real (s i)) =ᶠ[li] m) ContinuousAt.integral_sub_linear_isLittleO_ae._auto_1 →
              (fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m