no goals
ι : Type u_2
𝕜 : Type ?u.1482776
E : Type u_1
F : Type ?u.1482782
A : Type ?u.1482785
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
c ca cb : E
l l' la la' lb lb' : Filter ℝ
lt : Filter ι
μ : MeasureTheory.Measure ℝ
u v ua va ub vb : ι → ℝ
inst✝² : FTCFilter a la la'
inst✝¹ : FTCFilter b lb lb'
inst✝ : IsLocallyFiniteMeasure μ
hab : IntervalIntegrable f μ a b
hmeas : StronglyMeasurableAtFilter f la'
hf : Tendsto f (la' ⊓ Measure.ae μ) (𝓝 c)
hu : Tendsto u lt la
hv : Tendsto v lt la
⊢ (fun t => ((∫ (x : ℝ) in v t..b, f x ∂μ) - ∫ (x : ℝ) in u t..b, f x ∂μ) + ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t =>
    ∫ (x : ℝ) in u t..v t, 1 ∂μ
simpa using
  measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab hmeas
    stronglyMeasurableAt_bot hf ((tendsto_bot : Tendsto _ ⊥ (𝓝 (0 : E))).mono_left inf_le_left) hu
    hv (tendsto_const_pure : Tendsto _ _ (pure b)) tendsto_const_pure