awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, (↑y : EReal) < G' u
m M : ℝ
H : Ioo m M ⊆ {x : ℝ | (fun (u : ℝ) ↦ (↑y : EReal) < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
C1 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc t u), G' x < (↑∞ : EReal)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Icc t u))).EventuallyLE (β := ℝ) (fun (x : ℝ) ↦ y) fun (x : ℝ) ↦
    (G' x).toReal
have C2 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc t u), x ∈ Icc t u
Tactic: have C2 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), x ∈ Icc t u :=
              ae_restrict_mem measurableSet_Icc
-- 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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, (↑y : EReal) < G' u
m M : ℝ
H : Ioo m M ⊆ {x : ℝ | (fun (u : ℝ) ↦ (↑y : EReal) < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
C1 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc t u), G' x < (↑∞ : EReal)
C2 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc t u), x ∈ Icc t u
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Icc t u))).EventuallyLE (β := ℝ) (fun (x : ℝ) ↦ y) fun (x : ℝ) ↦
    (G' x).toReal
have h : ∀ (x : ℝ) (G'x : G' x < (↑∞ : EReal)) (hx : x ∈ Icc t u), y ≤ (G' x).toReal
Tactic: filter_upwards [C1, C2] with x G'x hx
-- 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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, (↑y : EReal) < G' u
m M : ℝ
H : Ioo m M ⊆ {x : ℝ | (fun (u : ℝ) ↦ (↑y : EReal) < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
C1 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc t u), G' x < (↑∞ : EReal)
C2 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc t u), x ∈ Icc t u
x : ℝ
G'x : G' x < (↑∞ : EReal)
hx : x ∈ Icc t u
⊢ y ≤ (G' x).toReal
have h : (↑y : EReal) ≤ (↑(G' x).toReal : EReal)
Tactic: apply EReal.coe_le_coe_iff.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, (↑y : EReal) < G' u
m M : ℝ
H : Ioo m M ⊆ {x : ℝ | (fun (u : ℝ) ↦ (↑y : EReal) < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
C1 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc t u), G' x < (↑∞ : EReal)
C2 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc t u), x ∈ Icc t u
x : ℝ
G'x : G' x < (↑∞ : EReal)
hx : x ∈ Icc t u
⊢ (↑y : EReal) ≤ (↑(G' x).toReal : EReal)
have this₁ : x ∈ Ioo m M
Tactic: have : x ∈ Ioo m M := by
              simp only [hm.trans_le hx.left,
                (hx.right.trans_lt hu.right).trans_le (min_le_left M b), mem_Ioo, and_self_iff]
-- 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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, (↑y : EReal) < G' u
m M : ℝ
H : Ioo m M ⊆ {x : ℝ | (fun (u : ℝ) ↦ (↑y : EReal) < G' u) x}
hm : m < t
hM : t < M
this_1 : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
C1 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc t u), G' x < (↑∞ : EReal)
C2 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc t u), x ∈ Icc t u
x : ℝ
G'x : G' x < (↑∞ : EReal)
hx : x ∈ Icc t u
this : x ∈ Ioo m M
⊢ (↑y : EReal) ≤ (↑(G' x).toReal : EReal)
have h : G' x = (↑(G' x).toReal : EReal)
Tactic: refine (H this).out.le.trans_eq ?_
-- 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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, (↑y : EReal) < G' u
m M : ℝ
H : Ioo m M ⊆ {x : ℝ | (fun (u : ℝ) ↦ (↑y : EReal) < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
⊢ (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
have y₁ : (u - t) * y = @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc t u)) fun (x : ℝ) ↦ y
Tactic: calc
        (u - t) * y = ∫ _ in Icc t u, y := by
          simp only [MeasureTheory.integral_const, MeasurableSet.univ, measureReal_restrict_apply,
            univ_inter, hu.left.le, Real.volume_real_Icc_of_le, smul_eq_mul]
        _ ≤ ∫ w in t..u, (G' w).toReal := by
          rw [intervalIntegral.integral_of_le hu.1.le, ← integral_Icc_eq_integral_Ioc]
          apply setIntegral_mono_ae_restrict
          · simp
          · exact IntegrableOn.mono_set G'int I
          · have C1 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), G' x < ∞ :=
              ae_mono (Measure.restrict_mono I le_rfl) G'lt_top
            have C2 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), x ∈ Icc t u :=
              ae_restrict_mem measurableSet_Icc
            filter_upwards [C1, C2] with x G'x hx
            apply EReal.coe_le_coe_iff.1
            have : x ∈ Ioo m M := by
              simp only [hm.trans_le hx.left,
                (hx.right.trans_lt hu.right).trans_le (min_le_left M b), mem_Ioo, and_self_iff]
            refine (H this).out.le.trans_eq ?_
            exact (EReal.coe_toReal G'x.ne (f_lt_G' x).ne_bot).symm
-- 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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, (↑y : EReal) < G' u
m M : ℝ
H : Ioo m M ⊆ {x : ℝ | (fun (u : ℝ) ↦ (↑y : EReal) < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
y₁ : (u - t) * y = @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc t u)) fun (x : ℝ) ↦ y
⊢ (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
have y₂ : LE.le (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc t u)) fun (x : ℝ) ↦ y)
  (∫ (w : ℝ) in t..u, (G' w).toReal)
Tactic: calc
        (u - t) * y = ∫ _ in Icc t u, y := by
          simp only [MeasureTheory.integral_const, MeasurableSet.univ, measureReal_restrict_apply,
            univ_inter, hu.left.le, Real.volume_real_Icc_of_le, smul_eq_mul]
        _ ≤ ∫ w in t..u, (G' w).toReal := by
          rw [intervalIntegral.integral_of_le hu.1.le, ← integral_Icc_eq_integral_Ioc]
          apply setIntegral_mono_ae_restrict
          · simp
          · exact IntegrableOn.mono_set G'int I
          · have C1 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), G' x < ∞ :=
              ae_mono (Measure.restrict_mono I le_rfl) G'lt_top
            have C2 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), x ∈ Icc t u :=
              ae_restrict_mem measurableSet_Icc
            filter_upwards [C1, C2] with x G'x hx
            apply EReal.coe_le_coe_iff.1
            have : x ∈ Ioo m M := by
              simp only [hm.trans_le hx.left,
                (hx.right.trans_lt hu.right).trans_le (min_le_left M b), mem_Ioo, and_self_iff]
            refine (H this).out.le.trans_eq ?_
            exact (EReal.coe_toReal G'x.ne (f_lt_G' x).ne_bot).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
⊢ ({t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty
have I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
Tactic: have I1 : ∀ᶠ u in 𝓝[>] t, (u - t) * y ≤ ∫ w in t..u, (G' w).toReal := by
      have B : ∀ᶠ u in 𝓝 t, (y : EReal) < G' u := G'cont.lowerSemicontinuousAt _ _ y_lt_G'
      rcases mem_nhds_iff_exists_Ioo_subset.1 B with ⟨m, M, ⟨hm, hM⟩, H⟩
      have : Ioo t (min M b) ∈ 𝓝[>] t := Ioo_mem_nhdsGT (lt_min hM ht.right.right)
      filter_upwards [this] with u hu
      have I : Icc t u ⊆ Icc a b := Icc_subset_Icc ht.2.1 (hu.2.le.trans (min_le_right _ _))
      calc
        (u - t) * y = ∫ _ in Icc t u, y := by
          simp only [MeasureTheory.integral_const, MeasurableSet.univ, measureReal_restrict_apply,
            univ_inter, hu.left.le, Real.volume_real_Icc_of_le, smul_eq_mul]
        _ ≤ ∫ w in t..u, (G' w).toReal := by
          rw [intervalIntegral.integral_of_le hu.1.le, ← integral_Icc_eq_integral_Ioc]
          apply setIntegral_mono_ae_restrict
          · simp
          · exact IntegrableOn.mono_set G'int I
          · have C1 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), G' x < ∞ :=
              ae_mono (Measure.restrict_mono I le_rfl) G'lt_top
            have C2 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), x ∈ Icc t u :=
              ae_restrict_mem measurableSet_Icc
            filter_upwards [C1, C2] with x G'x hx
            apply EReal.coe_le_coe_iff.1
            have : x ∈ Ioo m M := by
              simp only [hm.trans_le hx.left,
                (hx.right.trans_lt hu.right).trans_le (min_le_left M b), mem_Ioo, and_self_iff]
            refine (H this).out.le.trans_eq ?_
            exact (EReal.coe_toReal G'x.ne (f_lt_G' x).ne_bot).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
⊢ ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
have g'_lt_y : g' t < y
Tactic: have g'_lt_y : g' t < y := EReal.coe_lt_coe_iff.1 g'_lt_y'
-- 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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
g'_lt_y : g' t < y
⊢ ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
have h : ∀ (u : ℝ) (hu : slope g t u < y) (t_lt_u : u ∈ Ioi t), g u - g t ≤ (u - t) * y
Tactic: filter_upwards [(hderiv t ⟨ht.2.1, ht.2.2⟩).limsup_slope_le' (notMem_Ioi.2 le_rfl) g'_lt_y,
        self_mem_nhdsWithin] with u hu t_lt_u
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (hypothesis)
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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
g'_lt_y : g' t < y
u : ℝ
hu : slope g t u < y
t_lt_u : u ∈ Ioi t
⊢ g u - g t ≤ (u - t) * y
have this : (u - t) * slope g t u ≤ (u - t) * y
Tactic: have := mul_le_mul_of_nonneg_left hu.le (sub_pos.2 t_lt_u.out).le
-- 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
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : (↑(g' t) : EReal) < (↑y : EReal)
y_lt_G' : (↑y : EReal) < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
g'_lt_y : g' t < y
u : ℝ
hu : slope g t u < y
t_lt_u : u ∈ Ioi t
this : (u - t) * slope g t u ≤ (u - t) * y
⊢ g u - g t ≤ (u - t) * y
have h : ∀ (this : (u - t) • slope g t u ≤ (u - t) * y), g u - g t ≤ (u - t) * y
Tactic: rwa [← smul_eq_mul, sub_smul_slope] at this
Cleared hypotheses: this