-- Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean
theorem SimpleFunc.exists_upperSemicontinuous_le_lintegral_le (f : α →ₛ ℝ≥0)
    (int_f : (∫⁻ x, f x ∂μ) ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0) :
    ∃ g : α → ℝ≥0, (∀ x, g x ≤ f x) ∧ UpperSemicontinuous g ∧
      (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, g x ∂μ) + ε

Proof state:
case h_add.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∫⁻ (a : α), ↑(f₁ a) ∂μ + ∫⁻ (a : α), ↑(f₂ a) ∂μ ≤ ∫⁻ (a : α), ↑(g₁ a) ∂μ + ∫⁻ (a : α), ↑(g₂ a) ∂μ + ε

Tactic:
convert add_le_add g₁int g₂int using 1

Result:
case h.e'_4
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∫⁻ (a : α), ↑(g₁ a) ∂μ + ∫⁻ (a : α), ↑(g₂ a) ∂μ + ε =
    ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2 + (∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2)

Proof state:
case neg.intro.intro.intro.refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ⊤
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
x : α
⊢ F.indicator (fun x => c) x ≤ s.indicator (Function.const α c) x

Tactic:
exact Set.indicator_le_indicator_of_subset Fs (fun x => zero_le _) _

Result:
no goals

Proof state:
case h_add.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∃ g,
    (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε

Tactic:
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, ?_⟩

Result:
case h_add.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≤ ∫⁻ (x : α), ↑((fun x => g₁ x + g₂ x) x) ∂μ + ε

Proof state:
case h_add.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
⊢ ∃ g,
    (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε

Tactic:
rcases h₂ (ENNReal.add_ne_top.1 A).2 (ENNReal.half_pos ε0).ne' with
  ⟨g₂, f₂_le_g₂, g₂cont, g₂int⟩

Result:
case h_add.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∫⁻ (x : α), ↑(f₁ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
h₂ :
  ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤ →
    ∀ {ε : ℝ≥0∞},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
int_f : ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≠ ⊤
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ ≠ ⊤
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ f₁ x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(f₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ f₂ x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(f₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(g₂ x) ∂μ + ε / 2
⊢ ∃ g,
    (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε