Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: 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 ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
⊢ (fun t ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)) =o[lt] fun t ↦
    μ.real (Ioc (u t) (v t)) • 1 - μ.real (Ioc (v t) (u t)) • 1

Tactic:
refine ((A.trans_le fun t ↦ ?_).sub (B.trans_le fun t ↦ ?_)).congr_left fun t ↦ ?_

Goal state after:
case pos.refine_1
ι : 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 ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
t : ι
⊢ ‖μ.real (Ioc (u t) (v t))‖ ≤ ‖μ.real (Ioc (u t) (v t)) • 1 - μ.real (Ioc (v t) (u t)) • 1‖

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 ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
t : ι
⊢ ‖μ.real (Ioc (v t) (u t))‖ ≤ ‖μ.real (Ioc (u t) (v t)) • 1 - μ.real (Ioc (v t) (u t)) • 1‖

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 ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
t : ι
⊢ ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - μ.real (Ioc (u t) (v t)) • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
    ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)