awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : 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 :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
h : v t ≤ u t
⊢ ‖μ.real (Ioc (u t) (v t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : 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 :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
pos :
  u t ≤ v t →
    ‖μ.real (Ioc (v t) (u t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
pos₁ :
  v t ≤ u t →
    ‖μ.real (Ioc (v t) (u t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
⊢ ‖μ.real (Ioc (v t) (u t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖

Tactic:
cases le_total (u t) (v t)

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : 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 :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
h : u t ≤ v t
⊢ ‖μ.real (Ioc (v t) (u t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : 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 :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
h : v t ≤ u t
⊢ ‖μ.real (Ioc (v t) (u t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : 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 :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
pos :
  ∫ (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) =
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ) (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ) -
      (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)
⊢ ∫ (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)

Tactic:
simp_rw [intervalIntegral]

Premises used: intervalIntegral
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : 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 :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) 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) =
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ) (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ) -
      (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : CompleteSpace E
inst_3 : l'.IsMeasurablyGenerated
inst_4 : 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
huv : u ≤ᶠ[lt] v
x : ι
hx : u x ≤ v x
⊢ Eq.{u_3 + 1} (α := E)
    ((fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) x)
    ((fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - μ.real (Ioc (u t) (v t)) • c) x)

Tactic:
simp [integral_const', hx]

Premises used: intervalIntegral.integral_const'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : CompleteSpace E
inst_3 : l'.IsMeasurablyGenerated
inst_4 : 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
huv : u ≤ᶠ[lt] v
x : ι
hx : u x ≤ v x
⊢ Eq (α := ℝ) ((fun (t : ι) ↦ (∫ (x : ℝ) in u t..v t, 1 ∂μ : ℝ)) x) ((fun (t : ι) ↦ μ.real (Ioc (u t) (v t))) x)

Tactic:
simp [integral_const', hx]

Premises used: intervalIntegral.integral_const'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : CompleteSpace E
inst_3 : l'.IsMeasurablyGenerated
inst_4 : 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
huv : v ≤ᶠ[lt] u
t : ι
⊢ -(∫ (x : ℝ) in v t..u t, f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
    ∫ (x : ℝ) in u t..v t, f x ∂μ + μ.real (Ioc (v t) (u t)) • c

Tactic:
simp [integral_symm (u t), add_comm]

Premises used: intervalIntegral.integral_symm, add_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a : ℝ
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hu : Tendsto u lt l
hv : Tendsto v lt l
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
haveI := FTCFilter.meas_gen l
  measure_integral_sub_linear_isLittleO_of_tendsto_ae' hfm hf (FTCFilter.finiteAt_inner l) hu hv

Premises used: intervalIntegral.FTCFilter.finiteAt_inner, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a : ℝ
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : CompleteSpace E
inst_4 : FTCFilter a l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hu : Tendsto u lt l
hv : Tendsto v lt l
huv : u ≤ᶠ[lt] v
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - μ.real (Ioc (u t) (v t)) • c) fun (t : ι) ↦ μ.real (Ioc (u t) (v t))

Tactic:
haveI := FTCFilter.meas_gen l
  measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' hfm hf (FTCFilter.finiteAt_inner l) hu
    hv huv

Premises used: intervalIntegral.FTCFilter.finiteAt_inner, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a : ℝ
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : CompleteSpace E
inst_4 : FTCFilter a l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hu : Tendsto u lt l
hv : Tendsto v lt l
huv : v ≤ᶠ[lt] u
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ + μ.real (Ioc (v t) (u t)) • c) fun (t : ι) ↦ μ.real (Ioc (v t) (u t))

Tactic:
haveI := FTCFilter.meas_gen l
  measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' hfm hf (FTCFilter.finiteAt_inner l) hu
    hv huv

Premises used: intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge', intervalIntegral.FTCFilter.finiteAt_inner
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : 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 ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
⊢ la'.IsMeasurablyGenerated

Tactic:
haveI := FTCFilter.meas_gen la
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : 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 ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this : la'.IsMeasurablyGenerated
⊢ lb'.IsMeasurablyGenerated

Tactic:
haveI := FTCFilter.meas_gen lb
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : 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 ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this_1 : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in va t..vb t, f x ∂μ) (∫ (x : ℝ) in ua t..ub t, f x ∂μ) -
        HSub.hSub (α := E) (∫ (x : ℝ) in ub t..vb t, cb ∂μ) (∫ (x : ℝ) in ua t..va t, ca ∂μ))
    fun (t : ι) ↦ norm (E := ℝ) (∫ (x : ℝ) in ua t..va t, 1 ∂μ) + norm (E := ℝ) (∫ (x : ℝ) in ub t..vb t, 1 ∂μ)

Tactic:
((measure_integral_sub_linear_isLittleO_of_tendsto_ae hmeas_a ha_lim hua hva).neg_left.add_add
          (measure_integral_sub_linear_isLittleO_of_tendsto_ae hmeas_b hb_lim hub hvb)).congr'
      ?_ EventuallyEq.rfl

Premises used: Asymptotics.IsLittleO.neg_left, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae, Asymptotics.IsLittleO.congr', Asymptotics.IsLittleO.add_add, Filter.EventuallyEq.rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : 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 ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this_1 : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
hmeas_a₁ :
  EventuallyEq.{u_1, u_3} (β := E) lt
    (fun (x : ι) ↦
      -HSub.hSub (α := E) (∫ (x : ℝ) in ua x..va x, f x ∂μ) (∫ (x : ℝ) in ua x..va x, ca ∂μ) +
        HSub.hSub (α := E) (∫ (x : ℝ) in ub x..vb x, f x ∂μ) (∫ (x : ℝ) in ub x..vb x, cb ∂μ))
    fun (t : ι) ↦
    HSub.hSub (α := E) (∫ (x : ℝ) in va t..vb t, f x ∂μ) (∫ (x : ℝ) in ua t..ub t, f x ∂μ) -
      HSub.hSub (α := E) (∫ (x : ℝ) in ub t..vb t, cb ∂μ) (∫ (x : ℝ) in ua t..va t, ca ∂μ)
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in va t..vb t, f x ∂μ) (∫ (x : ℝ) in ua t..ub t, f x ∂μ) -
        HSub.hSub (α := E) (∫ (x : ℝ) in ub t..vb t, cb ∂μ) (∫ (x : ℝ) in ua t..va t, ca ∂μ))
    fun (t : ι) ↦ norm (E := ℝ) (∫ (x : ℝ) in ua t..va t, 1 ∂μ) + norm (E := ℝ) (∫ (x : ℝ) in ub t..vb t, 1 ∂μ)

Tactic:
refine
    ((measure_integral_sub_linear_isLittleO_of_tendsto_ae hmeas_a ha_lim hua hva).neg_left.add_add
          (measure_integral_sub_linear_isLittleO_of_tendsto_ae hmeas_b hb_lim hub hvb)).congr'
      ?_ EventuallyEq.rfl

Premises used: Asymptotics.IsLittleO.neg_left, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae, Asymptotics.IsLittleO.congr', Asymptotics.IsLittleO.add_add, Filter.EventuallyEq.rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : 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 ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this_1 : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
⊢ ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ua t) (va t)

Tactic:
have A : ∀ᶠ t in lt, IntervalIntegrable f μ (ua t) (va t) :=
    ha_lim.eventually_intervalIntegrable_ae hmeas_a (FTCFilter.finiteAt_inner la) hua hva
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : 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 ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this_1 : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
A : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ua t) (va t)
⊢ ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ a (ua t)

Tactic:
have A' : ∀ᶠ t in lt, IntervalIntegrable f μ a (ua t) :=
    ha_lim.eventually_intervalIntegrable_ae hmeas_a (FTCFilter.finiteAt_inner la)
      (tendsto_const_pure.mono_right FTCFilter.pure_le) hua
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : 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 ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this_1 : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
A : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ua t) (va t)
A' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ a (ua t)
⊢ ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ub t) (vb t)

Tactic:
have B : ∀ᶠ t in lt, IntervalIntegrable f μ (ub t) (vb t) :=
    hb_lim.eventually_intervalIntegrable_ae hmeas_b (FTCFilter.finiteAt_inner lb) hub hvb
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : 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 ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this_1 : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
A : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ua t) (va t)
A' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ a (ua t)
B : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ub t) (vb t)
⊢ ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ b (ub t)

Tactic:
have B' : ∀ᶠ t in lt, IntervalIntegrable f μ b (ub t) :=
    hb_lim.eventually_intervalIntegrable_ae hmeas_b (FTCFilter.finiteAt_inner lb)
      (tendsto_const_pure.mono_right FTCFilter.pure_le) hub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : 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 ι
μ : Measure ℝ
ua va ub vb : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas_a : StronglyMeasurableAtFilter f la' μ
hmeas_b : StronglyMeasurableAtFilter f lb' μ
ha_lim : Tendsto f (la' ⊓ ae μ) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae μ) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
this_1 : la'.IsMeasurablyGenerated
this : lb'.IsMeasurablyGenerated
A : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ua t) (va t)
A' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ a (ua t)
B : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (ub t) (vb t)
B' : ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ b (ub t)
h :
  ∀ (a_1 : ι) (ua_va : IntervalIntegrable f μ (ua a_1) (va a_1)) (a_ua : IntervalIntegrable f μ a (ua a_1))
    (ub_vb : IntervalIntegrable f μ (ub a_1) (vb a_1)) (b_ub : IntervalIntegrable f μ b (ub a_1)),
    -HSub.hSub (α := E) (∫ (x : ℝ) in ua a_1..va a_1, f x ∂μ) (∫ (x : ℝ) in ua a_1..va a_1, ca ∂μ) +
        HSub.hSub (α := E) (∫ (x : ℝ) in ub a_1..vb a_1, f x ∂μ) (∫ (x : ℝ) in ub a_1..vb a_1, cb ∂μ) =
      HSub.hSub (α := E) (∫ (x : ℝ) in va a_1..vb a_1, f x ∂μ) (∫ (x : ℝ) in ua a_1..ub a_1, f x ∂μ) -
        HSub.hSub (α := E) (∫ (x : ℝ) in ub a_1..vb a_1, cb ∂μ) (∫ (x : ℝ) in ua a_1..va a_1, ca ∂μ)
⊢ EventuallyEq.{u_1, u_3} (β := E) lt
    (fun (x : ι) ↦
      -HSub.hSub (α := E) (∫ (x : ℝ) in ua x..va x, f x ∂μ) (∫ (x : ℝ) in ua x..va x, ca ∂μ) +
        HSub.hSub (α := E) (∫ (x : ℝ) in ub x..vb x, f x ∂μ) (∫ (x : ℝ) in ub x..vb x, cb ∂μ))
    fun (t : ι) ↦
    HSub.hSub (α := E) (∫ (x : ℝ) in va t..vb t, f x ∂μ) (∫ (x : ℝ) in ua t..ub t, f x ∂μ) -
      HSub.hSub (α := E) (∫ (x : ℝ) in ub t..vb t, cb ∂μ) (∫ (x : ℝ) in ua t..va t, ca ∂μ)

Tactic:
filter_upwards [A, A', B, B'] with _ ua_va a_ua ub_vb b_ub