awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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)
⊢ 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 ∂μ)
have B : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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)
⊢ 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 ∂μ)
have B' : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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)
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: filter_upwards [A, A', B, B'] with _ ua_va a_ua ub_vb b_ub
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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 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 ∂μ)
have 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 ∂μ)
Tactic: rw [← integral_interval_sub_interval_comm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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)
⊢ -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 ∂μ)
have h₃ : IntervalIntegrable f μ (ub a_1) (ua a_1)
Tactic: rw [← integral_interval_sub_interval_comm']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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)
⊢ HasStrictFDerivAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (a, b)
have 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‖
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)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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)
have 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)
Tactic: refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
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)
⊢ HasStrictFDerivAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (a, b)
have 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
Tactic: refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
⊢ HasFDerivWithinAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (s ×ˢ t) (a, b)
have this : IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s] a ×ˢ 𝓝[t] b)
  (fun (t : ℝ × ℝ) ↦
    HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
  fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
Tactic: have :=
    integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hf hmeas_a hmeas_b ha hb
      (tendsto_const_pure.mono_right FTCFilter.pure_le : Tendsto _ _ (𝓝[s] a)) tendsto_fst
      (tendsto_const_pure.mono_right FTCFilter.pure_le : Tendsto _ _ (𝓝[t] b)) tendsto_snd
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s] a ×ˢ 𝓝[t] b)
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ HasFDerivWithinAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (s ×ˢ t) (a, b)
have this₁ : IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s ×ˢ t] (a, b))
  (fun (t : ℝ × ℝ) ↦
    HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
  fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
Tactic: rw [← nhdsWithin_prod_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s ×ˢ t] (a, b))
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ HasFDerivWithinAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (s ×ˢ t) (a, b)
have refine_1 : ∀ (x : ℝ × ℝ),
  HSub.hSub (α := E) (∫ (x : ℝ) in x.1..x.2, f x) (∫ (x : ℝ) in a..b, f x) - ((x.2 - b) • cb - (x.1 - a) • ca) =
    HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (x : ℝ) in x.1..x.2, f x) (∫ (x : ℝ) in (a, b).1..(a, b).2, f x))
      ((HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca) : (a : ℝ × ℝ) → E)
          (x - (a, b)) :
        E)
Tactic: refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s ×ˢ t] (a, b))
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
refine_1 :
  ∀ (x : ℝ × ℝ),
    HSub.hSub (α := E) (∫ (x : ℝ) in x.1..x.2, f x) (∫ (x : ℝ) in a..b, f x) - ((x.2 - b) • cb - (x.1 - a) • ca) =
      HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (x : ℝ) in x.1..x.2, f x) (∫ (x : ℝ) in (a, b).1..(a, b).2, f x))
        ((HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca) : (a : ℝ × ℝ) → E)
            (x - (a, b)) :
          E)
⊢ HasFDerivWithinAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (s ×ˢ t) (a, b)
have refine_2 : IsBigO (E := ℝ) (F := ℝ × ℝ) (𝓝[s ×ˢ t] (a, b)) (fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖) fun (x' : ℝ × ℝ) ↦ x' - (a, b)
Tactic: refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) (𝓝[t] a)
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝[t] a) volume
ha : Tendsto f (𝓝[t] a ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
⊢ HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) (-c) s a
have simp : HasDerivWithinAt (fun (u : ℝ) ↦ -∫ (x : ℝ) in b..u, f x) (-c) s a
Tactic: simp only [integral_symm b]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
have refine : ∀ (ε : ℝ) (εpos : 0 < ε), g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε
Tactic: refine le_of_forall_pos_le_add fun ε εpos => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
⊢ g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε
have rcases : ∀ (G' : ℝ → EReal) (f_lt_G' : ∀ (x : ℝ), (↑(φ x) : EReal) < G' x) (G'cont : LowerSemicontinuous G')
  (G'int :
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (G' x).toReal)
      (Measure.restrict volume (Icc a b)))
  (G'lt_top : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), G' x < ⊤)
  (hG' :
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ (G' x).toReal) <
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ φ x) + ε),
  g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε
Tactic: rcases exists_lt_lowerSemicontinuous_integral_lt φ φint εpos with
    ⟨G', f_lt_G', G'cont, G'int, G'lt_top, hG'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), (↑(φ x) : EReal) < G' x
G'cont : LowerSemicontinuous G'
G'int :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (G' x).toReal) (Measure.restrict volume (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), G' x < ⊤
hG' :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ (G' x).toReal) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ φ x) + ε
s : Set ℝ := {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
⊢ ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g t - g a, ∫ (u : ℝ) in a..t, (G' u).toReal)) (Icc a b)
have rw : ∀ (hcont : ContinuousOn g [[a, b]]) (hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x)
  (φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume) (hφg : ∀ x ∈ Ico a b, g' x ≤ φ x)
  (ε : ℝ) (εpos : 0 < ε) (G' : ℝ → EReal) (f_lt_G' : ∀ (x : ℝ), (↑(φ x) : EReal) < G' x)
  (G'cont : LowerSemicontinuous G')
  (G'int :
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (G' x).toReal) (Measure.restrict volume [[a, b]]))
  (G'lt_top : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), G' x < ⊤)
  (hG' :
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ (G' x).toReal) <
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ φ x) + ε),
  ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g t - g a, ∫ (u : ℝ) in a..t, (G' u).toReal)) [[a, b]]
Tactic: rw [← uIcc_of_le hab] at G'int hcont ⊢
Cleared hypotheses: hcont, hderiv, φint, hφg, ε, εpos, G', f_lt_G', G'cont, G'int, G'lt_top, hG', s