-- Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean
theorem SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge (f : α →ₛ ℝ≥0) {ε : ℝ≥0∞}
    (ε0 : ε ≠ 0) :
    ∃ g : α → ℝ≥0, (∀ x, f x ≤ g x) ∧ LowerSemicontinuous g ∧
      (∫⁻ x, g x ∂μ) ≤ (∫⁻ x, f 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₁ :
  ∀ {ε : ℝ≥0∞},
    ε ≠ 0 → ∃ g, (∀ (x : α), f₁ x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(f₁ x) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞},
    ε ≠ 0 → ∃ g, (∀ (x : α), f₂ x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(f₂ x) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), f₁ x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(g₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(f₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), f₂ x ≤ g₂ x
g₂cont : LowerSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(g₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(f₂ x) ∂μ + ε / 2
⊢ ∃ g,
    (∀ (x : α), (f₁ + f₂) x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((f₁ + f₂) 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₁ :
  ∀ {ε : ℝ≥0∞},
    ε ≠ 0 → ∃ g, (∀ (x : α), f₁ x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(f₁ x) ∂μ + ε
h₂ :
  ∀ {ε : ℝ≥0∞},
    ε ≠ 0 → ∃ g, (∀ (x : α), f₂ x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(f₂ x) ∂μ + ε
ε : ℝ≥0∞
ε0 : ε ≠ 0
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), f₁ x ≤ g₁ x
g₁cont : LowerSemicontinuous g₁
g₁int : ∫⁻ (x : α), ↑(g₁ x) ∂μ ≤ ∫⁻ (x : α), ↑(f₁ x) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), f₂ x ≤ g₂ x
g₂cont : LowerSemicontinuous g₂
g₂int : ∫⁻ (x : α), ↑(g₂ x) ∂μ ≤ ∫⁻ (x : α), ↑(f₂ x) ∂μ + ε / 2
⊢ ∫⁻ (x : α), ↑((fun x => g₁ x + g₂ x) x) ∂μ ≤ ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ + ε

Proof state:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ⊤
hc : ¬c = 0
ne_top : μ s ≠ ⊤
⊢ ∃ g,
    (∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ g x) ∧
      LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
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

Result:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ⊤
hc : ¬c = 0
ne_top : μ s ≠ ⊤
this : μ s < μ s + ε / ↑c
⊢ ∃ g,
    (∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ g x) ∧
      LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Proof state:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ⊤
hc : c = 0
⊢ ∃ g,
    (∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ g x) ∧
      LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
refine ⟨fun _ => 0, ?_, lowerSemicontinuous_const, ?_⟩

Result:
case pos.refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ⊤
hc : c = 0
⊢ ∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ (fun x => 0) x

case pos.refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ⊤
hc : c = 0
⊢ ∫⁻ (x : α), ↑((fun x => 0) x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Proof state:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ∫⁻ (x : α), ↑(f x) ∂μ = ⊤
x : α
⊢ (piecewise s hs (const α c) (const α 0)) x ≤ (fun x => c) x

Tactic:
simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
  Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise]

Result:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ∫⁻ (x : α), ↑(f x) ∂μ = ⊤
x : α
⊢ s.indicator (Function.const α c) x ≤ c

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ∫⁻ (x : α), ↑(f x) ∂μ = ⊤
⊢ ∫⁻ (x : α), ↑((fun x => c) x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
simp only [f, _root_.top_add, le_top, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ¬∫⁻ (x : α), ↑(f x) ∂μ = ⊤
hc : ¬c = 0
ne_top : μ s ≠ ⊤
this✝ : μ s < μ s + ε / ↑c
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : μ u < μ s + ε / ↑c
this : ↑c * μ u ≤ ↑c * μ s + ε
⊢ ∫⁻ (x : α), ↑(u.indicator (fun x => c) x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
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]

Result:
no goals