-- Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean
theorem exists_lt_lowerSemicontinuous_integral_lt [SigmaFinite μ] (f : α → ℝ) (hf : Integrable f μ)
    {ε : ℝ} (εpos : 0 < ε) :
    ∃ g : α → EReal,
      (∀ x, (f x : EReal) < g x) ∧
      LowerSemicontinuous g ∧
      Integrable (fun x => EReal.toReal (g x)) μ ∧
      (∀ᵐ x ∂μ, g x < ⊤) ∧ (∫ x, EReal.toReal (g x) ∂μ) < (∫ x, f x ∂μ) + ε

Proof state:
case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := ⟨ε / 2, ⋯⟩
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => (f x).toNNReal
int_fp : Integrable (fun x => ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable (fun x => (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => (-f x).toNNReal
int_fm : Integrable (fun x => ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x => ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
x : α
⊢ ↑↑(f x).toNNReal < ↑(gp x)

Tactic:
simp only [EReal.coe_ennreal_lt_coe_ennreal_iff]

Result:
case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := ⟨ε / 2, ⋯⟩
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => (f x).toNNReal
int_fp : Integrable (fun x => ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable (fun x => (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => (-f x).toNNReal
int_fm : Integrable (fun x => ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x => ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
x : α
⊢ ↑(f x).toNNReal < gp x

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := ⟨ε / 2, ⋯⟩
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => (f x).toNNReal
int_fp : Integrable (fun x => ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable (fun x => (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => (-f x).toNNReal
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (fun x => (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε

Tactic:
have int_fm : Integrable (fun x => (fm x : ℝ)) μ := hf.neg.real_toNNReal

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := ⟨ε / 2, ⋯⟩
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => (f x).toNNReal
int_fp : Integrable (fun x => ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable (fun x => (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => (-f x).toNNReal
int_fm : Integrable (fun x => ↑(fm x)) μ
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (fun x => (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε

Proof state:
case hf
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := ⟨ε / 2, ⋯⟩
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => (f x).toNNReal
int_fp : Integrable (fun x => ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable (fun x => (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => (-f x).toNNReal
int_fm : Integrable (fun x => ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x => ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
⊢ LowerSemicontinuous fun z => ↑(gp z)

Tactic:
exact continuous_coe_ennreal_ereal.comp_lowerSemicontinuous gpcont fun x y hxy =>
    EReal.coe_ennreal_le_coe_ennreal_iff.2 hxy

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := ⟨ε / 2, ⋯⟩
δpos : 0 < δ
fp : α → ℝ≥0 := fun x => (f x).toNNReal
int_fp : Integrable (fun x => ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ⊤
gp_integrable : Integrable (fun x => (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + (fun a => ↑a) δ
fm : α → ℝ≥0 := fun x => (-f x).toNNReal
int_fm : Integrable (fun x => ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x => ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - (fun a => ↑a) δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x => ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
⊢ UpperSemicontinuous fun z => ↑(gm z)

Tactic:
exact ENNReal.continuous_coe.comp_upperSemicontinuous gmcont fun x y hxy =>
    ENNReal.coe_le_coe.2 hxy

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (fun x => (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε

Tactic:
let δ : ℝ≥0 := ⟨ε / 2, (half_pos εpos).le⟩

Result:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := ⟨ε / 2, ⋯⟩
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (fun x => (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε