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
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)
⊢ Membership.mem (γ := Set ℝ) {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} x
have g₁ : g x - g a = g t - g a + (g x - g t)
Tactic: calc
      g x - g a = g t - g a + (g x - g t) := by abel
      _ ≤ (∫ w in a..t, (G' w).toReal) + ∫ w in t..x, (G' w).toReal := add_le_add ht.1 hx
      _ = ∫ w in a..x, (G' w).toReal := by
        apply integral_add_adjacent_intervals
        · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le ht.2.1]
          exact IntegrableOn.mono_set G'int
            (Ioc_subset_Icc_self.trans (Icc_subset_Icc le_rfl ht.2.2.le))
        · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x.1.le]
          apply IntegrableOn.mono_set G'int
          exact Ioc_subset_Icc_self.trans (Icc_subset_Icc ht.2.1 (h'x.2.trans (min_le_right _ _)))
-- 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)
g₁ : g x - g a = g t - g a + (g x - g t)
⊢ Membership.mem (γ := Set ℝ) {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} x
have g₂ : HAdd.hAdd (α := ℝ) (∫ (w : ℝ) in a..t, (G' w).toReal) (∫ (w : ℝ) in t..x, (G' w).toReal) =
  ∫ (w : ℝ) in a..x, (G' w).toReal
Tactic: calc
      g x - g a = g t - g a + (g x - g t) := by abel
      _ ≤ (∫ w in a..t, (G' w).toReal) + ∫ w in t..x, (G' w).toReal := add_le_add ht.1 hx
      _ = ∫ w in a..x, (G' w).toReal := by
        apply integral_add_adjacent_intervals
        · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le ht.2.1]
          exact IntegrableOn.mono_set G'int
            (Ioc_subset_Icc_self.trans (Icc_subset_Icc le_rfl ht.2.2.le))
        · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x.1.le]
          apply IntegrableOn.mono_set G'int
          exact Ioc_subset_Icc_self.trans (Icc_subset_Icc ht.2.1 (h'x.2.trans (min_le_right _ _)))
-- 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
main : Icc a b ⊆ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal}
⊢ ∫ (y : ℝ) in a..b, (G' y).toReal ≤ (∫ (y : ℝ) in a..b, φ y) + ε
have h : Eq (α := ℝ) (∫ (y : ℝ) in a..b, (G' y).toReal)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ (G' x).toReal)
Tactic: convert! hG'.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
main : Icc a b ⊆ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal}
h :
  Eq (α := ℝ) (∫ (y : ℝ) in a..b, (G' y).toReal)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ (G' x).toReal)
⊢ ∫ (y : ℝ) in a..b, (G' y).toReal ≤ (∫ (y : ℝ) in a..b, φ y) + ε
have h₁ : Eq (α := ℝ) (∫ (y : ℝ) in a..b, φ y)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ φ x)
Tactic: convert! hG'.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
main : Icc a b ⊆ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal}
⊢ Eq (α := ℝ) (∫ (y : ℝ) in a..b, (G' y).toReal)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ (G' x).toReal)
have h : Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ (G' x).toReal)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ (G' x).toReal)
Tactic: rw [intervalIntegral.integral_of_le hab]
-- 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
main : Icc a b ⊆ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal}
⊢ Eq (α := ℝ) (∫ (y : ℝ) in a..b, φ y)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ φ x)
have h : Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ φ x)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ φ x)
Tactic: rw [intervalIntegral.integral_of_le hab]
-- 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
main : Icc a b ⊆ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal}
⊢ g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε
have g₁ : ∫ (y : ℝ) in a..b, (G' y).toReal ≤ (∫ (y : ℝ) in a..b, φ y) + ε
Tactic: calc
    g b - g a ≤ ∫ y in a..b, (G' y).toReal := main (right_mem_Icc.2 hab)
    _ ≤ (∫ y in a..b, φ y) + ε := by
      convert! hG'.le <;>
        · rw [intervalIntegral.integral_of_le hab]
          simp only [integral_Icc_eq_integral_Ioc', Real.volume_singleton]
-- 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
have inl : ∀ (hab : a ≤ a) (hcont : ContinuousOn g (Icc a a)) (hderiv : ∀ x ∈ Ioo a a, HasDerivWithinAt g (g' x) (Ioi x) x)
  (φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a a) volume) (hφg : ∀ x ∈ Ioo a a, g' x ≤ φ x),
  g a - g a ≤ ∫ (y : ℝ) in a..a, φ y
Tactic: obtain rfl | a_lt_b := hab.eq_or_lt
Cleared hypotheses: b, hab, hcont, hderiv, φint, hφg
-- 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
inl :
  ∀ (hab : a ≤ a) (hcont : ContinuousOn g (Icc a a)) (hderiv : ∀ x ∈ Ioo a a, HasDerivWithinAt g (g' x) (Ioi x) x)
    (φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a a) volume) (hφg : ∀ x ∈ Ioo a a, g' x ≤ φ x),
    g a - g a ≤ ∫ (y : ℝ) in a..a, φ y
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
have inr : ∀ (a_lt_b : a < b), g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
Tactic: obtain rfl | a_lt_b := hab.eq_or_lt
-- 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
⊢ ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g b - g t, ∫ (u : ℝ) in t..b, φ u)) (Icc a b)
have rw : ∀ (hcont : ContinuousOn g [[a, b]]) (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x)
  (φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ [[a, b]] volume) (hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x)
  (a_lt_b : a < b), ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g b - g t, ∫ (u : ℝ) in t..b, φ u)) [[a, b]]
Tactic: rw [← uIcc_of_le hab] at hcont φint ⊢
Cleared hypotheses: hcont, hderiv, φint, hφg, a_lt_b, s
-- 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
⊢ IsClosed s
have this : ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g b - g t, ∫ (u : ℝ) in t..b, φ u)) (Icc a b)
Tactic: have : ContinuousOn (fun t => (g b - g t, ∫ u in t..b, φ u)) (Icc a b) := by
      rw [← uIcc_of_le hab] at hcont φint ⊢
      exact (continuousOn_const.sub hcont).prodMk (continuousOn_primitive_interval_left φint)
-- 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
this : ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g b - g t, ∫ (u : ℝ) in t..b, φ u)) (Icc a b)
⊢ IsClosed s
have simp : IsClosed (Icc a b ∩ {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u})
Tactic: simp only [s, inter_comm]
-- 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
have s_closed : IsClosed s
Tactic: have s_closed : IsClosed s := by
    have : ContinuousOn (fun t => (g b - g t, ∫ u in t..b, φ u)) (Icc a b) := by
      rw [← uIcc_of_le hab] at hcont φint ⊢
      exact (continuousOn_const.sub hcont).prodMk (continuousOn_primitive_interval_left φint)
    simp only [s, inter_comm]
    exact this.preimage_isClosed_of_isClosed isClosed_Icc isClosed_le_prod
-- 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
⊢ closure (Ioc a b) ⊆ s
have apply : Ioc a b ⊆ s
Tactic: apply s_closed.closure_subset_iff.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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ Ioc a b
⊢ t ∈ s
have refine : Membership.mem (γ := Set ℝ) {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} t
Tactic: refine ⟨?_, ⟨ht.1.le, ht.2⟩⟩
-- 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
have A : closure (Ioc a b) ⊆ s
Tactic: have A : closure (Ioc a b) ⊆ s := by
    apply s_closed.closure_subset_iff.2
    intro t ht
    refine ⟨?_, ⟨ht.1.le, ht.2⟩⟩
    exact
      sub_le_integral_of_hasDeriv_right_of_le_Ico ht.2 (hcont.mono (Icc_subset_Icc ht.1.le le_rfl))
        (fun x hx => hderiv x ⟨ht.1.trans_le hx.1, hx.2⟩)
        (φint.mono_set (Icc_subset_Icc ht.1.le le_rfl)) fun x hx => hφg x ⟨ht.1.trans_le hx.1, hx.2⟩
-- 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x
a_lt_b : a < b
s : Set ℝ := {t : ℝ | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b
s_closed : IsClosed s
A : closure (Ioc a b) ⊆ s
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
have A₁ : Icc a b ⊆ s
Tactic: rw [closure_Ioc a_lt_b.ne] at A
Cleared hypotheses: A
-- 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ ∫ (y : ℝ) in a..b, φ y ≤ g b - g a
have rw : -(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y
Tactic: rw [← neg_le_neg_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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ -(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y
have h : -(g b - g a) = -g b - -g a
Tactic: convert!
    sub_le_integral_of_hasDeriv_right_of_le hab hcont.neg (fun x hx => (hderiv x hx).neg) φint.neg
      fun x hx => neg_le_neg (hφg x hx) using 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
h : -(g b - g a) = -g b - -g a
⊢ -(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y
have h₁ : Eq (α := ℝ) (-∫ (y : ℝ) in a..b, φ y) (∫ (y : ℝ) in a..b, (-φ) y)
Tactic: convert!
    sub_le_integral_of_hasDeriv_right_of_le hab hcont.neg (fun x hx => (hderiv x hx).neg) φint.neg
      fun x hx => neg_le_neg (hφg x hx) using 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 ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) φ (Icc a b) volume
hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x
⊢ Eq (α := ℝ) (-∫ (y : ℝ) in a..b, φ y) (∫ (y : ℝ) in a..b, (-φ) y)
have h : Eq (α := ℝ) (∫ (x : ℝ) in a..b, -φ x) (∫ (y : ℝ) in a..b, (-φ) y)
Tactic: simp only [← integral_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have refine : ∀ (g : StrongDual ℝ E),
  Eq (α := ℝ) ((g : (a : E) → ℝ) (∫ (y : ℝ) in a..b, f' y) : ℝ) ((g : (a : E) → ℝ) (f b - f a) : ℝ)
Tactic: refine (SeparatingDual.eq_iff_forall_dual_eq (R := ℝ)).2 fun g => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : StrongDual ℝ E
⊢ Eq (α := ℝ) ((g : (a : E) → ℝ) (∫ (y : ℝ) in a..b, f' y) : ℝ) ((g : (a : E) → ℝ) (f b - f a) : ℝ)
have rw : ∫ (x : ℝ) in a..b, (g : (a : E) → ℝ) (f' x) =
  HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) (f b) : ℝ) ((g : (a : E) → ℝ) (f a) : ℝ)
Tactic: rw [← g.intervalIntegral_comp_comm f'int, g.map_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have inl : ∀ (hab : a ≤ b), ∫ (y : ℝ) in a..b, f' y = f b - f a
Tactic: rcases le_total a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hint : IntervalIntegrable f' volume a b
inl : ∀ (hab : a ≤ b), ∫ (y : ℝ) in a..b, f' y = f b - f a
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a
have inr : ∀ (hab : b ≤ a), ∫ (y : ℝ) in a..b, f' y = f b - f a
Tactic: rcases le_total a b with hab | hab