no goals
ι : Type u_2
𝕜 : Type ?u.1641367
E : Type u_1
F : Type ?u.1641373
A : Type ?u.1641376
inst✝⁴ : NormedAddCommGroup E
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c ca cb : E
l l' la la' lb lb' : Filter ℝ
lt : Filter ι
a b z : ℝ
u v ua ub va vb : ι → ℝ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hab : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter f la'
hf : Tendsto f (la' ⊓ Measure.ae volume) (𝓝 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) + (v t - u t) • c) =o[lt] (v - u)
simpa only [integral_const, smul_eq_mul, mul_one] using
  measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left hab hmeas hf hu hv