Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: 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 φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
⊢ g b - g a ≤ (∫ (y : ℝ) in a..b, φ y) + ε

Tactic:
have main : Icc a b ⊆ {t | g t - g a ≤ ∫ u in a..t, (G' u).toReal} := by
    -- to show that the set `s` is all `[a, b]`, it suffices to show that any point `t` in `s`
    -- with `t < b` admits another point in `s` slightly to its right
    -- (this is a sort of real induction).
    refine s_closed.Icc_subset_of_forall_exists_gt
      (by simp only [integral_same, mem_ofPred_eq, sub_self, le_rfl]) fun t ht v t_lt_v => ?_
    obtain ⟨y, g'_lt_y', y_lt_G'⟩ : ∃ y : ℝ, (g' t : EReal) < y ∧ (y : EReal) < G' t :=
      EReal.lt_iff_exists_real_btwn.1 ((EReal.coe_le_coe_iff.2 (hφg t ht.2)).trans_lt (f_lt_G' t))
    -- bound from below the increase of `∫ x in a..u, G' x` on the right of `t`, using the lower
    -- semicontinuity of `G'`.
    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
    -- bound from above the increase of `g u - g a` on the right of `t`, using the derivative at `t`
    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
    -- combine the previous two bounds to show that `g u - g a` increases less quickly than
    -- `∫ x in a..u, G' x`.
    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
    have I4 : ∀ᶠ u in 𝓝[>] t, u ∈ Ioc t (min v b) := Ioc_mem_nhdsGT <| lt_min t_lt_v ht.2.2
    -- choose a point `x` slightly to the right of `t` which satisfies the above bound
    rcases (I3.and I4).exists with ⟨x, hx, h'x⟩
    -- we check that it belongs to `s`, essentially by construction
    refine ⟨x, ?_, Ioc_subset_Ioc le_rfl (min_le_left _ _) h'x⟩
    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 _ _)))

Goal state after:
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 φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ 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) + ε