-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α →ₛ ℝ≥0
ε : ℝ≥0∞
ε0 : ε ≠ 0
const :
  ∀ (c : ℝ≥0) {s : Set α} (hs : MeasurableSet s) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x ≤ g x) ∧
        LowerSemicontinuous g ∧
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤
            ∫⁻ (x : α),
                (↑((piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ +
              ε
add :
  ∀ ⦃f₁ f₂ : α →ₛ ℝ≥0⦄,
    Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
        (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0)) →
      ∀
        (h₁ :
          ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
            ∃ (g : α → ℝ≥0),
              (∀ (x : α), (f₁ : (a : α) → ℝ≥0) x ≤ g x) ∧
                LowerSemicontinuous g ∧
                  ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε)
        (h₂ :
          ∀ {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
            ∃ (g : α → ℝ≥0),
              (∀ (x : α), (f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
                LowerSemicontinuous g ∧
                  ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε)
        {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
        ∃ (g : α → ℝ≥0),
          (∀ (x : α), (f₁ + f₂ : (a : α) → ℝ≥0) x ≤ g x) ∧
            LowerSemicontinuous g ∧
              ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), (f : (a : α) → ℝ≥0) x ≤ g x) ∧
      LowerSemicontinuous g ∧ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((f : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε

Tactic:
induction f using MeasureTheory.SimpleFunc.induction generalizing ε with
  | @const c s hs =>
    let f := SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)
    by_cases h : ∫⁻ x, f x ∂μ = ⊤
    · refine
        ⟨fun _ => c, fun x => ?_, lowerSemicontinuous_const, by
          simp only [f, _root_.top_add, le_top, h]⟩
      simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise]
      exact Set.indicator_le_self _ _ _
    by_cases hc : c = 0
    · refine ⟨fun _ => 0, ?_, lowerSemicontinuous_const, ?_⟩
      · classical
        simp only [hc, Set.indicator_zero', Pi.zero_apply, SimpleFunc.const_zero, imp_true_iff,
          SimpleFunc.coe_zero, Set.piecewise_eq_indicator,
          SimpleFunc.coe_piecewise, le_zero_iff]
      · simp only [lintegral_const, zero_mul, zero_le, ENNReal.coe_zero]
    have ne_top : μ s ≠ ⊤ := by
      classical
      simpa [f, hs, hc, lt_top_iff_ne_top, SimpleFunc.coe_const,
        Function.const_apply, lintegral_const, ENNReal.coe_indicator, Set.univ_inter,
        ENNReal.coe_ne_top, MeasurableSet.univ, ENNReal.mul_eq_top, SimpleFunc.const_zero,
        lintegral_indicator, ENNReal.coe_eq_zero, Ne, not_false_iff,
        SimpleFunc.coe_zero, Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise,
        restrict_apply] using h
    have : μ s < μ s + ε / c := by
      have : (0 : ℝ≥0∞) < ε / c := ENNReal.div_pos_iff.2 ⟨ε0, ENNReal.coe_ne_top⟩
      simpa using ENNReal.add_lt_add_left ne_top this
    obtain ⟨u, su, u_open, μu⟩ : ∃ (u : _), u ⊇ s ∧ IsOpen u ∧ μ u < μ s + ε / c :=
      s.exists_isOpen_lt_of_lt _ this
    refine ⟨Set.indicator u fun _ => c,
      fun x => ?_, u_open.lowerSemicontinuous_indicator zero_le, ?_⟩
    · simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, ← Function.const_def]
      grw [su]
    · suffices (c : ℝ≥0∞) * μ u ≤ c * μ s + ε by
        classical
        simpa only [ENNReal.coe_indicator, u_open.measurableSet, lintegral_indicator,
          lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, const_zero,
          coe_piecewise, coe_const, coe_zero, Set.piecewise_eq_indicator, Function.const_apply, hs]
      calc
        (c : ℝ≥0∞) * μ u ≤ c * (μ s + ε / c) := by grw [μu]
        _ = c * μ s + ε := by
          simp_rw [mul_add]
          rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
          simpa using hc
  | @add f₁ f₂ _ h₁ h₂ =>
    rcases h₁ (ENNReal.half_pos ε0).ne' with ⟨g₁, f₁_le_g₁, g₁cont, g₁int⟩
    rcases h₂ (ENNReal.half_pos ε0).ne' with ⟨g₂, f₂_le_g₂, g₂cont, g₂int⟩
    refine
      ⟨fun x => g₁ x + g₂ x, fun x => add_le_add (f₁_le_g₁ x) (f₂_le_g₂ x), g₁cont.add g₂cont, ?_⟩
    simp only [SimpleFunc.coe_add, ENNReal.coe_add, Pi.add_apply]
    rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal,
      lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal]
    convert! add_le_add g₁int g₂int using 1
    conv_lhs => rw [← ENNReal.add_halves ε]
    abel

Premises used: zero_le, MeasureTheory.lintegral_const, MeasureTheory.SimpleFunc.const, le_zero_iff, MeasureTheory.SimpleFunc.coe_add, MulZeroClass.zero_mul, MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, Pi.zero_apply, ENNReal.coe_add, Set.indicator_zero', imp_true_iff, Pi.add_apply, ENNReal.coe_zero, Function.const_def, Set.indicator_le_self, ENNReal.add_halves, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.SimpleFunc.coe_const