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

Tactic:
induction f using MeasureTheory.SimpleFunc.induction generalizing ε with
  | @const c s hs =>
    classical
    by_cases hc : c = 0
    · exact ⟨fun _ => 0, by simp [hc, upperSemicontinuous_const]⟩
    have μs_lt_top : μ s < ∞ := by simpa [hs, hc, ENNReal.mul_eq_top, lt_top_iff_ne_top] using int_f
    have : (0 : ℝ≥0∞) < ε / c := ENNReal.div_pos_iff.2 ⟨ε0, ENNReal.coe_ne_top⟩
    obtain ⟨F, Fs, F_closed, μF⟩ : ∃ (F : _), F ⊆ s ∧ IsClosed F ∧ μ s < μ F + ε / c :=
      hs.exists_isClosed_lt_add μs_lt_top.ne this.ne'
    refine
      ⟨Set.indicator F fun _ => c, fun x => ?_, F_closed.upperSemicontinuous_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 [Fs]
    · suffices (c : ℝ≥0∞) * μ s ≤ c * μ F + ε by
        simpa only [hs, F_closed.measurableSet, SimpleFunc.coe_const, Function.const_apply,
          lintegral_const, ENNReal.coe_indicator, Set.univ_inter, MeasurableSet.univ,
          SimpleFunc.const_zero, lintegral_indicator, SimpleFunc.coe_zero,
          Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, Measure.restrict_apply]
      calc
        (c : ℝ≥0∞) * μ s ≤ c * (μ F + ε / c) := by grw [μF]
        _ = c * μ F + ε := by
          simp_rw [mul_add]
          rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
          simpa using hc
  | @add f₁ f₂ _ h₁ h₂ =>
    have A : ((∫⁻ x : α, f₁ x ∂μ) + ∫⁻ x : α, f₂ x ∂μ) ≠ ⊤ := by
      rwa [← lintegral_add_left f₁.measurable.coe_nnreal_ennreal]
    rcases h₁ (ENNReal.add_ne_top.1 A).1 (ENNReal.half_pos ε0).ne' with
      ⟨g₁, f₁_le_g₁, g₁cont, g₁int⟩
    rcases h₂ (ENNReal.add_ne_top.1 A).2 (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: MeasureTheory.SimpleFunc.const, MeasureTheory.SimpleFunc.coe_add, MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, ENNReal.coe_add, Pi.add_apply, Function.const_def, ENNReal.add_halves, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.SimpleFunc.coe_const