awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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 b (𝓝[s] b) (𝓝[t] b)
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝[t] b) volume
hb : Tendsto f (𝓝[t] b ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
hs : UniqueDiffWithinAt ℝ s b
⊢ derivWithin (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) s b = c

Tactic:
(integral_hasDerivWithinAt_of_tendsto_ae_right hf hmeas hb).derivWithin hs

Premises used: intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right, HasDerivWithinAt.derivWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter b (𝓝[s] b) (𝓝[t] b)
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝[t] b) volume
hb : ContinuousWithinAt f t b
hs : UniqueDiffWithinAt ℝ s b
⊢ derivWithin (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) s b = f b

Tactic:
(integral_hasDerivWithinAt_right hf hmeas hb).derivWithin hs

Premises used: intervalIntegral.integral_hasDerivWithinAt_right, HasDerivWithinAt.derivWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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)
simp : HasDerivWithinAt (fun (u : ℝ) ↦ -∫ (x : ℝ) in b..u, f x) (-c) s a
⊢ HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) (-c) s a

Tactic:
simp only [integral_symm b]

Premises used: intervalIntegral.integral_symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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 b..u, f x) (-c) s a

Tactic:
(integral_hasDerivWithinAt_of_tendsto_ae_right hf.symm hmeas ha).neg

Premises used: intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right, HasDerivWithinAt.neg, IntervalIntegrable.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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 b..u, f x) (-c) s a

Tactic:
exact (integral_hasDerivWithinAt_of_tendsto_ae_right hf.symm hmeas ha).neg

Premises used: intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right, HasDerivWithinAt.neg, IntervalIntegrable.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) (𝓝[t] a)
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝[t] a) volume
ha : ContinuousWithinAt f t a
⊢ HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) (-f a) s a

Tactic:
integral_hasDerivWithinAt_of_tendsto_ae_left hf hmeas (ha.mono_left inf_le_left)

Premises used: intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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)
hs : UniqueDiffWithinAt ℝ s a
⊢ derivWithin (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) s a = -c

Tactic:
(integral_hasDerivWithinAt_of_tendsto_ae_left hf hmeas ha).derivWithin hs

Premises used: intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left, HasDerivWithinAt.derivWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) (𝓝[t] a)
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝[t] a) volume
ha : ContinuousWithinAt f t a
hs : UniqueDiffWithinAt ℝ s a
⊢ derivWithin (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) s a = -f a

Tactic:
(integral_hasDerivWithinAt_left hf hmeas ha).derivWithin hs

Premises used: intervalIntegral.integral_hasDerivWithinAt_left, HasDerivWithinAt.derivWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a : ℝ
hcont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Differentiable.{0, 0, u_3} ℝ (F := E) fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x

Tactic:
fun _ ↦
  (integral_hasDerivAt_right (hcont.intervalIntegrable _ _)
    hcont.aestronglyMeasurable.stronglyMeasurableAtFilter hcont.continuousAt).differentiableAt

Premises used: Differentiable, HasDerivAt.differentiableAt, Continuous.intervalIntegrable, Continuous.continuousAt, MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, intervalIntegral.integral_hasDerivAt_right, Continuous.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a : ℝ
s : Set ℝ
hcont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ DifferentiableOn.{0, 0, u_3} ℝ (F := E) (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) s

Tactic:
(differentiable_integral_of_continuous hcont).differentiableOn

Premises used: intervalIntegral.differentiable_integral_of_continuous, Differentiable.differentiableOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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

Tactic:
le_of_forall_pos_le_add fun ε εpos => ?_

Premises used: le_of_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
refine : ∀ (ε : ℝ) (εpos : 0 < ε), g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε
⊢ g b - g a ≤ ∫ (y : ℝ) in a..b, φ y

Tactic:
refine le_of_forall_pos_le_add fun ε εpos => ?_

Premises used: le_of_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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 < ε
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) + ε
⊢ 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'⟩

Premises used: MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
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]]
⊢ ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g t - g a, ∫ (u : ℝ) in a..t, (G' u).toReal)) (Icc a b)

Tactic:
rw [← uIcc_of_le hab] at G'int hcont ⊢

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
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) + ε
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)) [[a, b]]

Tactic:
(hcont.sub continuousOn_const).prodMk (continuousOn_primitive_interval G'int)

Premises used: intervalIntegral.continuousOn_primitive_interval, ContinuousOn.sub, continuousOn_const, ContinuousOn.prodMk
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
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) + ε
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)) [[a, b]]

Tactic:
exact (hcont.sub continuousOn_const).prodMk (continuousOn_primitive_interval G'int)

Premises used: intervalIntegral.continuousOn_primitive_interval, ContinuousOn.sub, continuousOn_const, ContinuousOn.prodMk
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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)

Tactic:
have : ContinuousOn (fun t => (g t - g a, ∫ u in a..t, (G' u).toReal)) (Icc a b) := by
      rw [← uIcc_of_le hab] at G'int hcont ⊢
      exact (hcont.sub continuousOn_const).prodMk (continuousOn_primitive_interval G'int)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
this : ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g t - g a, ∫ (u : ℝ) in a..t, (G' u).toReal)) (Icc a b)
simp : IsClosed (Icc a b ∩ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal})
⊢ IsClosed s

Tactic:
simp only [s, inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
this : ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g t - g a, ∫ (u : ℝ) in a..t, (G' u).toReal)) (Icc a b)
⊢ IsClosed (Icc a b ∩ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal})

Tactic:
this.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, Set.Mem, setOf, intervalIntegral, OrderClosedTopology.isClosed_le', isClosed_Icc, Set.preimage
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
this : ContinuousOn (Y := ℝ × ℝ) (fun (t : ℝ) ↦ (g t - g a, ∫ (u : ℝ) in a..t, (G' u).toReal)) (Icc a b)
⊢ IsClosed (Icc a b ∩ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal})

Tactic:
exact this.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, OrderClosedTopology.isClosed_le', isClosed_Icc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
⊢ IsClosed s

Tactic:
have s_closed : IsClosed s := by
    have : ContinuousOn (fun t => (g t - g a, ∫ u in a..t, (G' u).toReal)) (Icc a b) := by
      rw [← uIcc_of_le hab] at G'int hcont ⊢
      exact (hcont.sub continuousOn_const).prodMk (continuousOn_primitive_interval G'int)
    simp only [s, inter_comm]
    exact this.preimage_isClosed_of_isClosed isClosed_Icc OrderClosedTopology.isClosed_le'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
⊢ Membership.mem (γ := Set ℝ) {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} a

Tactic:
simp only [integral_same, mem_setOf_eq, sub_self, le_rfl]

Premises used: le_rfl, sub_self, Set.mem_setOf_eq, intervalIntegral.integral_same
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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
refine :
  ∀ (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),
    ({t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty
⊢ Icc a b ⊆ {t : ℝ | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal}

Tactic:
refine s_closed.Icc_subset_of_forall_exists_gt
      (by simp only [integral_same, mem_setOf_eq, sub_self, le_rfl]) fun t ht v t_lt_v => ?_

Premises used: IsClosed.Icc_subset_of_forall_exists_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
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' t) : EReal) < (↑y : EReal) ∧ (↑y : EReal) < G' t

Tactic:
EReal.lt_iff_exists_real_btwn.1 ((EReal.coe_le_coe_iff.2 (hφg t ht.2)).trans_lt (f_lt_G' t))

Premises used: Iff.mpr, EReal.coe_le_coe_iff, And.right, Iff.mp, LE.le.trans_lt, EReal.lt_iff_exists_real_btwn