∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ}
  {ca cb : E} {la la' lb lb' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {ua va ub vb : ι → ℝ}
  [MeasureTheory.IsLocallyFiniteMeasure μ] [intervalIntegral.FTCFilter a la la'] [intervalIntegral.FTCFilter b lb lb'],
  IntervalIntegrable f μ a b →
    StronglyMeasurableAtFilter f la' μ →
      StronglyMeasurableAtFilter f lb' μ →
        Filter.Tendsto f (la' ⊓ MeasureTheory.ae μ) (nhds ca) →
          Filter.Tendsto f (lb' ⊓ MeasureTheory.ae μ) (nhds cb) →
            Filter.Tendsto ua lt la →
              Filter.Tendsto va lt la →
                Filter.Tendsto ub lt lb →
                  Filter.Tendsto vb lt lb →
                    (fun t =>
                        ∫ (x : ℝ) in va t..vb t, f x ∂μ - ∫ (x : ℝ) in ua t..ub t, f x ∂μ -
                          (∫ (x : ℝ) in ub t..vb t, cb ∂μ - ∫ (x : ℝ) in ua t..va t, ca ∂μ)) =o[lt]
                      fun t => ‖∫ (x : ℝ) in ua t..va t, 1 ∂μ‖ + ‖∫ (x : ℝ) in ub t..vb t, 1 ∂μ‖