-- 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 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) ∂μ = ⊤
⊢ ∃ 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 _ => c, fun x => ?_, lowerSemicontinuous_const, by
    simp only [f, _root_.top_add, le_top, h]⟩

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 : α
⊢ (piecewise s hs (const α c) (const α 0)) x ≤ (fun x => c) x

Proof state:
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

Tactic:
classical
simp only [hc, Set.indicator_zero', Pi.zero_apply, SimpleFunc.const_zero, imp_true_iff,
  eq_self_iff_true, SimpleFunc.coe_zero, Set.piecewise_eq_indicator,
  SimpleFunc.coe_piecewise, le_zero_iff]

Result:
no goals

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₁ :
  ∀ {ε : ℝ≥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,
    (∀ (x : α), (f₁ + f₂) x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((f₁ + f₂) x) ∂μ + ε

Tactic:
rcases h₂ (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₁ :
  ∀ {ε : ℝ≥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) ∂μ + ε

Proof state:
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

Tactic:
simp only [hc, Set.indicator_zero', Pi.zero_apply, SimpleFunc.const_zero, imp_true_iff,
  eq_self_iff_true, SimpleFunc.coe_zero, Set.piecewise_eq_indicator,
  SimpleFunc.coe_piecewise, le_zero_iff]

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 : 0 < ε / ↑c
⊢ μ s < μ s + ε / ↑c

Tactic:
simpa using ENNReal.add_lt_add_left ne_top this

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₁ :
  ∀ {ε : ℝ≥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
⊢ ∫⁻ (a : α), ↑(g₁ a) ∂μ + ∫⁻ (a : α), ↑(g₂ a) ∂μ ≤ ∫⁻ (a : α), ↑(f₁ a) ∂μ + ∫⁻ (a : α), ↑(f₂ 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₁ :
  ∀ {ε : ℝ≥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
⊢ ∫⁻ (a : α), ↑(f₁ a) ∂μ + ∫⁻ (a : α), ↑(f₂ a) ∂μ + ε =
    ∫⁻ (x : α), ↑(f₁ x) ∂μ + ε / 2 + (∫⁻ (x : α), ↑(f₂ x) ∂μ + ε / 2)

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
⊢ μ s ≠ ⊤

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

Result:
no goals