awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : ∀ (this : (u - t) • slope g t u ≤ (u - t) * y), g u - g t ≤ (u - t) * y
⊢ g u - g t ≤ (u - t) * y
have h₁ : ∀ (this : g u -ᵥ g t ≤ (u - t) * y), g u - g t ≤ (u - t) * y
Tactic: rwa [← smul_eq_mul, sub_smul_slope] at this
Cleared hypotheses: this
-- 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
⊢ ({t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty
have I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
Tactic: have I2 : ∀ᶠ u in 𝓝[>] t, g u - g t ≤ (u - t) * y := by
      have g'_lt_y : g' t < y := EReal.coe_lt_coe_iff.1 g'_lt_y'
      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
      have := mul_le_mul_of_nonneg_left hu.le (sub_pos.2 t_lt_u.out).le
      rwa [← smul_eq_mul, sub_smul_slope] at this
-- 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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
⊢ ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (u : ℝ) ↦ (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            Membership.mem (γ := Set ℝ) {x : ℝ | (fun (u : ℝ) ↦ g u - g t ≤ (u - t) * y) x} x →
              Membership.mem (γ := Set ℝ) {x : ℝ | (fun (u : ℝ) ↦ g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal) x} x}
          x}
    a
Tactic: filter_upwards [I1, I2] with u hu1 hu2 using hu2.trans hu1
-- 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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (u : ℝ) ↦ (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              Membership.mem (γ := Set ℝ) {x : ℝ | (fun (u : ℝ) ↦ g u - g t ≤ (u - t) * y) x} x →
                Membership.mem (γ := Set ℝ) {x : ℝ | (fun (u : ℝ) ↦ g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal) x} x}
            x}
      a
⊢ ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
have h₁ : ∀ (a : ℝ),
  (a - t) * y ≤ ∫ (w : ℝ) in t..a, (G' w).toReal →
    g a - g t ≤ (a - t) * y → g a - g t ≤ ∫ (w : ℝ) in t..a, (G' w).toReal
Tactic: filter_upwards [I1, I2] with u hu1 hu2 using hu2.trans hu1
-- 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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
⊢ ({t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty
have I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
Tactic: have I3 : ∀ᶠ u in 𝓝[>] t, g u - g t ≤ ∫ w in t..u, (G' w).toReal := by
      filter_upwards [I1, I2] with u hu1 hu2 using hu2.trans hu1
-- 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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
⊢ ({t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty
have I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
Tactic: have I4 : ∀ᶠ u in 𝓝[>] t, u ∈ Ioc t (min v b) := Ioc_mem_nhdsGT <| lt_min t_lt_v ht.2.2
-- 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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
⊢ ({t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty
have rcases : ∀ (x : ℝ) (hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal) (h'x : x ∈ Ioc t (min v b)),
  ({t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty
Tactic: rcases (I3.and I4).exists with ⟨x, hx, h'x⟩
-- 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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
x : ℝ
hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal
h'x : x ∈ Ioc t (min v b)
⊢ ({t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty
have refine : Membership.mem (γ := Set ℝ) {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} x
Tactic: refine ⟨x, ?_, Ioc_subset_Ioc le_rfl (min_le_left _ _) h'x⟩
-- 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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
x : ℝ
hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal
h'x : x ∈ Ioc t (min v b)
⊢ HAdd.hAdd (α := ℝ) (∫ (w : ℝ) in a..t, (G' w).toReal) (∫ (w : ℝ) in t..x, (G' w).toReal) =
    ∫ (w : ℝ) in a..x, (G' w).toReal
have hab₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (G' x).toReal) volume a t
Tactic: apply integral_add_adjacent_intervals
-- 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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
x : ℝ
hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal
h'x : x ∈ Ioc t (min v b)
hab₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (G' x).toReal) volume a t
⊢ HAdd.hAdd (α := ℝ) (∫ (w : ℝ) in a..t, (G' w).toReal) (∫ (w : ℝ) in t..x, (G' w).toReal) =
    ∫ (w : ℝ) in a..x, (G' w).toReal
have hbc : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (G' x).toReal) volume t x
Tactic: apply integral_add_adjacent_intervals
-- 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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
x : ℝ
hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal
h'x : x ∈ Ioc t (min v b)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (G' x).toReal) volume a t
have hab₁ : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ (G' x).toReal) (Ioc a t) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le ht.2.1]
-- 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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
x : ℝ
hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal
h'x : x ∈ Ioc t (min v b)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (G' x).toReal) volume t x
have hbc : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ (G' x).toReal) (Ioc t x) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x.1.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
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
x : ℝ
hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal
h'x : x ∈ Ioc t (min v b)
⊢ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ (G' x).toReal) (Ioc t x) volume
have hbc : Ioc t x ⊆ Icc a b
Tactic: apply IntegrableOn.mono_set G'int