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
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)
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)
h :
  -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 ub a_1..vb a_1, f x ∂μ) (∫ (x : ℝ) in ua a_1..va 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 ∂μ)
h₁ : IntervalIntegrable f μ (ub a_1) (vb a_1)
h₂ : IntervalIntegrable f μ (ua a_1) (va a_1)
h₃ : IntervalIntegrable f μ (ub a_1) (ua 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 ∂μ)

Tactic:
rw [← integral_interval_sub_interval_comm']

Premises used: intervalIntegral.integral_interval_sub_interval_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 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)
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 ub a_1..vb a_1, f x ∂μ) (∫ (x : ℝ) in ua a_1..va 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 ∂μ)

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
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)
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)
⊢ IntervalIntegrable f μ (ub a_1) (vb a_1)

Tactic:
ub_vb
-- 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)
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)
⊢ IntervalIntegrable f μ (ua a_1) (va a_1)

Tactic:
ua_va
-- 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)
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)
⊢ IntervalIntegrable f μ (ub a_1) (ua a_1)

Tactic:
b_ub.symm.trans <| hab.symm.trans a_ua

Premises used: IntervalIntegrable.symm, IntervalIntegrable.trans
-- 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)
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)
⊢ IntervalIntegrable f μ (ub a_1) (vb a_1)

Tactic:
exacts [ub_vb, ua_va, b_ub.symm.trans <| hab.symm.trans a_ua]

Premises used: IntervalIntegrable.symm, IntervalIntegrable.trans
-- 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 : ℝ
c : E
lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter b lb lb'
hab : IntervalIntegrable f μ a b
hmeas : StronglyMeasurableAtFilter f lb' μ
hf : Tendsto f (lb' ⊓ ae μ) (𝓝 c)
hu : Tendsto u lt lb
hv : Tendsto v lt lb
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in a..v t, f x ∂μ) (∫ (x : ℝ) in a..u t, f x ∂μ) - ∫ (x : ℝ) in u t..v t, c ∂μ)
    fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
simpa using
    measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab stronglyMeasurableAt_bot
      hmeas ((tendsto_bot : Tendsto _ ⊥ (𝓝 (0 : E))).mono_left inf_le_left) hf
      (tendsto_const_pure : Tendsto _ _ (pure a)) tendsto_const_pure hu hv

Premises used: stronglyMeasurableAt_bot, Filter.tendsto_bot, intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae, Filter.Tendsto.mono_left, inf_le_left, Filter.tendsto_const_pure
-- 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 : ℝ
c : E
la la' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : FTCFilter a la la'
hab : IntervalIntegrable f μ a b
hmeas : StronglyMeasurableAtFilter f la' μ
hf : Tendsto f (la' ⊓ ae μ) (𝓝 c)
hu : Tendsto u lt la
hv : Tendsto v lt la
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in v t..b, f x ∂μ) (∫ (x : ℝ) in u t..b, f x ∂μ) + ∫ (x : ℝ) in u t..v t, c ∂μ)
    fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
simpa using
    measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab hmeas
      stronglyMeasurableAt_bot hf ((tendsto_bot : Tendsto _ ⊥ (𝓝 (0 : E))).mono_left inf_le_left) hu
      hv (tendsto_const_pure : Tendsto _ _ (pure b)) tendsto_const_pure

Premises used: stronglyMeasurableAt_bot, Filter.tendsto_bot, intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae, Filter.Tendsto.mono_left, inf_le_left, Filter.tendsto_const_pure
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
a : ℝ
inst_3 : FTCFilter a l l'
hfm : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f l' volume
hf : Tendsto f (l' ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
u v : ι → ℝ
hu : Tendsto u lt l
hv : Tendsto v lt l
⊢ IsLittleO.{u_1, u_3, 0} (E := E) lt (fun (t : ι) ↦ (∫ (x : ℝ) in u t..v t, f x) - (v t - u t) • c) (v - u)

Tactic:
simpa [integral_const] using measure_integral_sub_linear_isLittleO_of_tendsto_ae hfm hf hu hv

Premises used: intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae, intervalIntegral.integral_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la la' lb lb' : Filter ℝ
lt : Filter ι
a b : ℝ
ua ub va vb : ι → ℝ
inst_3 : FTCFilter a la la'
inst_4 : FTCFilter b lb lb'
hab : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la' volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb' volume
ha_lim : Tendsto f (la' ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb_lim : Tendsto f (lb' ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
hua : Tendsto ua lt la
hva : Tendsto va lt la
hub : Tendsto ub lt lb
hvb : Tendsto vb lt lb
⊢ 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) -
        ((vb t - ub t) • cb - (va t - ua t) • ca))
    fun (t : ι) ↦ ‖va t - ua t‖ + ‖vb t - ub t‖

Tactic:
simpa [integral_const]
    using measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab hmeas_a hmeas_b
      ha_lim hb_lim hua hva hub hvb

Premises used: intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae, intervalIntegral.integral_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
lb lb' : Filter ℝ
lt : Filter ι
a b : ℝ
u v : ι → ℝ
inst_3 : FTCFilter b lb lb'
hab : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb' volume
hf : Tendsto f (lb' ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
hu : Tendsto u lt lb
hv : Tendsto v lt lb
⊢ IsLittleO.{u_1, u_3, 0} (E := E) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in a..v t, f x) (∫ (x : ℝ) in a..u t, f x) - (v t - u t) • c) (v - u)

Tactic:
simpa only [integral_const, smul_eq_mul, mul_one] using
    measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right hab hmeas hf hu hv

Premises used: intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right, smul_eq_mul, mul_one, intervalIntegral.integral_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
la la' : Filter ℝ
lt : Filter ι
a b : ℝ
u v : ι → ℝ
inst_3 : FTCFilter a la la'
hab : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la' volume
hf : Tendsto f (la' ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
hu : Tendsto u lt la
hv : Tendsto v lt la
⊢ IsLittleO.{u_1, u_3, 0} (E := E) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in v t..b, f x) (∫ (x : ℝ) in u t..b, f x) + (v t - u t) • c) (v - u)

Tactic:
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

Premises used: intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left, smul_eq_mul, mul_one, intervalIntegral.integral_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
⊢ IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝 ((a, b), a, b))
    (fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1.1..t.1.2, f x) (∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca))
    fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖

Tactic:
have :=
    integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hf hmeas_a hmeas_b ha hb
      (continuous_snd.fst.tendsto ((a, b), (a, b)))
      (continuous_fst.fst.tendsto ((a, b), (a, b)))
      (continuous_snd.snd.tendsto ((a, b), (a, b)))
      (continuous_fst.snd.tendsto ((a, b), (a, b)))
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝 ((a, b), a, b))
    (fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1.1..t.1.2, f x) (∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca))
    fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ HasStrictFDerivAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (a, b)

Tactic:
.of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_

Premises used: Asymptotics.IsLittleO.congr_left, setOf, HasStrictFDerivAt.of_isLittleO, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝 ((a, b), a, b))
    (fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1.1..t.1.2, f x) (∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca))
    fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
refine_1 :
  ∀ (x : (ℝ × ℝ) × ℝ × ℝ),
    HSub.hSub (α := E) (∫ (x : ℝ) in x.1.1..x.1.2, f x) (∫ (x : ℝ) in x.2.1..x.2.2, f x) -
        ((x.1.2 - x.2.2) • cb - (x.1.1 - x.2.1) • ca) =
      HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (x : ℝ) in x.1.1..x.1.2, f x) (∫ (x : ℝ) in x.2.1..x.2.2, f x))
        ((HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca) : (a : ℝ × ℝ) → E)
            (x.1 - x.2) :
          E)
refine_2 :
  IsBigO (E := ℝ) (F := ℝ × ℝ) (𝓝 ((a, b), a, b)) (fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖)
    fun (p : (ℝ × ℝ) × ℝ × ℝ) ↦ p.1 - p.2
⊢ HasStrictFDerivAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (a, b)

Tactic:
refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_

Premises used: Asymptotics.IsLittleO.congr_left, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝 ((a, b), a, b))
    (fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1.1..t.1.2, f x) (∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca))
    fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ ∀ (x : (ℝ × ℝ) × ℝ × ℝ),
    HSub.hSub (α := E) (∫ (x : ℝ) in x.1.1..x.1.2, f x) (∫ (x : ℝ) in x.2.1..x.2.2, f x) -
        ((x.1.2 - x.2.2) • cb - (x.1.1 - x.2.1) • ca) =
      HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (x : ℝ) in x.1.1..x.1.2, f x) (∫ (x : ℝ) in x.2.1..x.2.2, f x))
        ((HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca) : (a : ℝ × ℝ) → E)
            (x.1 - x.2) :
          E)

Tactic:
simp [sub_smul]

Premises used: sub_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝 ((a, b), a, b))
    (fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1.1..t.1.2, f x) (∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca))
    fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ IsBigO (E := ℝ) (F := ℝ × ℝ) (𝓝 ((a, b), a, b)) (fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖)
    fun (p : (ℝ × ℝ) × ℝ × ℝ) ↦ p.1 - p.2

Tactic:
isBigO_fst_prod.norm_left.add isBigO_snd_prod.norm_left

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.isBigO_fst_prod, Asymptotics.IsBigO.add, Asymptotics.isBigO_snd_prod
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝 ((a, b), a, b))
    (fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1.1..t.1.2, f x) (∫ (x : ℝ) in t.2.1..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca))
    fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ IsBigO (E := ℝ) (F := ℝ × ℝ) (𝓝 ((a, b), a, b)) (fun (t : (ℝ × ℝ) × ℝ × ℝ) ↦ ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖)
    fun (p : (ℝ × ℝ) × ℝ × ℝ) ↦ p.1 - p.2

Tactic:
exact isBigO_fst_prod.norm_left.add isBigO_snd_prod.norm_left

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.isBigO_fst_prod, Asymptotics.IsBigO.add, Asymptotics.isBigO_snd_prod
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : ContinuousAt f a
hb : ContinuousAt f b
⊢ HasStrictFDerivAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) (f b)) (smulRight (fst ℝ ℝ ℝ) (f a))) (a, b)

Tactic:
integral_hasStrictFDerivAt_of_tendsto_ae hf hmeas_a hmeas_b (ha.mono_left inf_le_left)
    (hb.mono_left inf_le_left)

Premises used: intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae, Filter.Tendsto.mono_left, inf_le_left