-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae' [IsMeasurablyGenerated l']
    [TendstoIxxClass Ioc l l'] (hfm : StronglyMeasurableAtFilter f l' μ)
    (hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)) (hl : μ.FiniteAtFilter l') (hu : Tendsto u lt l)
    (hv : Tendsto v lt l) :
    (fun t => (∫ x in u t..v t, f x ∂μ) - ∫ _ in u t..v t, c ∂μ) =o[lt] fun t =>
      ∫ _ in u t..v t, (1 : ℝ) ∂μ

Proof state:
case pos.refine_3
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (u i) (v i))).toReal
B :
  (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (v i) (u i))).toReal
t : ι
⊢ ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - (μ (Ioc (u t) (v t))).toReal • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - (μ (Ioc (v t) (u t))).toReal • c) =
    ∫ (x : ℝ) in u t..v t, f x ∂μ - ((μ (Ioc (u t) (v t))).toReal • c - (μ (Ioc (v t) (u t))).toReal • c)

Tactic:
simp_rw [intervalIntegral]

Result:
case pos.refine_3
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (u i) (v i))).toReal
B :
  (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (v i) (u i))).toReal
t : ι
⊢ ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - (μ (Ioc (u t) (v t))).toReal • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - (μ (Ioc (v t) (u t))).toReal • c) =
    ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - ∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ -
      ((μ (Ioc (u t) (v t))).toReal • c - (μ (Ioc (v t) (u t))).toReal • c)

Proof state:
case pos.refine_2
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (u i) (v i))).toReal
B :
  (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (v i) (u i))).toReal
t : ι
⊢ ‖(μ (Ioc (v t) (u t))).toReal‖ ≤ ‖(μ (Ioc (u t) (v t))).toReal • 1 - (μ (Ioc (v t) (u t))).toReal • 1‖

Tactic:
cases le_total (u t) (v t) <;> simp [*]

Result:
no goals

Proof state:
case pos.refine_3
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (u i) (v i))).toReal
B :
  (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (v i) (u i))).toReal
t : ι
⊢ ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - (μ (Ioc (u t) (v t))).toReal • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - (μ (Ioc (v t) (u t))).toReal • c) =
    ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - ∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ -
      ((μ (Ioc (u t) (v t))).toReal • c - (μ (Ioc (v t) (u t))).toReal • c)

Tactic:
abel

Result:
no goals

Proof state:
case pos
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (u i) (v i))).toReal
B :
  (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (v i) (u i))).toReal
⊢ (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
simp_rw [integral_const', sub_smul]

Result:
case pos
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (u i) (v i))).toReal
B :
  (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (v i) (u i))).toReal
⊢ (fun t =>
      ∫ (x : ℝ) in u t..v t, f x ∂μ - ((μ (Ioc (u t) (v t))).toReal • c - (μ (Ioc (v t) (u t))).toReal • c)) =o[lt]
    fun t => (μ (Ioc (u t) (v t))).toReal • 1 - (μ (Ioc (v t) (u t))).toReal • 1

Proof state:
case pos
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (u i) (v i))).toReal
⊢ (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
have B := hf.integral_sub_linear_isLittleO_ae hfm hl (hv.Ioc hu)

Result:
case pos
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (u i) (v i))).toReal
B :
  (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i =>
    (μ (Ioc (v i) (u i))).toReal
⊢ (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ