-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
pos :
  ∀ (hc : c = 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧
          ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
            ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
neg neg₁ :
  ∀ (hc : ¬c = 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧
          ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
            ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
neg₂ :
  ∀ (hc : ¬c = 0) (μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧
          ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
            ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
neg₃ :
  ∀ (hc : ¬c = 0) (μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
    (this : 0 < ε / (↑c : ℝ≥0∞)),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧
          ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
            ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have neg₄ : ∀ (hc : ¬c = 0) (μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
  (this : 0 < ε / (↑c : ℝ≥0∞)) (F : Set α) (Fs : F ⊆ s) (F_closed : IsClosed F)
  (μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: 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