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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ ∃ g,
    (∀ (x : α), g x < ↑(f x)) ∧
      UpperSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ (∫ (x : α), f x ∂μ) < (∫ (x : α), EReal.toReal (g x) ∂μ) + ε
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
⊢ ∃ g,
    (∀ (x : α), g x < ↑(f x)) ∧
      UpperSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ (∫ (x : α), f x ∂μ) < (∫ (x : α), EReal.toReal (g x) ∂μ) + ε
rcases exists_lt_lowerSemicontinuous_integral_lt (fun x => -f x) hf.neg εpos with
  ⟨g, g_lt_f, gcont, g_integrable, g_lt_top, gint⟩
case intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ ∀ (x : α), (fun x => -g x) x < ↑(f x)

case intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ UpperSemicontinuous fun x => -g x

case intro.intro.intro.intro.intro.refine'_3
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ Integrable fun x => EReal.toReal ((fun x => -g x) x)

case intro.intro.intro.intro.intro.refine'_4
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ ∀ᵐ (x : α) ∂μ, ⊥ < (fun x => -g x) x

case intro.intro.intro.intro.intro.refine'_5
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ (∫ (x : α), f x ∂μ) < (∫ (x : α), EReal.toReal ((fun x => -g x) x) ∂μ) + ε
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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ ∃ g,
    (∀ (x : α), g x < ↑(f x)) ∧
      UpperSemicontinuous g ∧
        (Integrable fun x => EReal.toReal (g x)) ∧
          (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ (∫ (x : α), f x ∂μ) < (∫ (x : α), EReal.toReal (g x) ∂μ) + ε
refine' ⟨fun x => -g x, _, _, _, _, _⟩
no goals
case intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ ∀ (x : α), (fun x => -g x) x < ↑(f x)
exact fun x => EReal.neg_lt_iff_neg_lt.1 (by simpa only [EReal.coe_neg] using g_lt_f x)
no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
x : α
⊢ -↑(f x) < g x
simpa only [EReal.coe_neg] using g_lt_f x
no goals
case intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ UpperSemicontinuous fun x => -g x
exact
  continuous_neg.comp_lowerSemicontinuous_antitone gcont fun x y hxy =>
    EReal.neg_le_neg_iff.2 hxy
case h.e'_5.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
x✝ : α
⊢ EReal.toReal ((fun x => -g x) x✝) = (-fun x => EReal.toReal (g x)) x✝
case intro.intro.intro.intro.intro.refine'_3
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ Integrable fun x => EReal.toReal ((fun x => -g x) x)
convert g_integrable.neg
no goals
case h.e'_5.h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
x✝ : α
⊢ EReal.toReal ((fun x => -g x) x✝) = (-fun x => EReal.toReal (g x)) x✝
simp
no goals
case intro.intro.intro.intro.intro.refine'_4
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ ∀ᵐ (x : α) ∂μ, ⊥ < (fun x => -g x) x
simpa [bot_lt_iff_ne_bot, lt_top_iff_ne_top] using g_lt_top
case intro.intro.intro.intro.intro.refine'_5
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ((∫ (a : α), f a ∂μ) + ∫ (x : α), EReal.toReal (g x) ∂μ) < ε
⊢ (∫ (x : α), f x ∂μ) < (∫ (x : α), EReal.toReal ((fun x => -g x) x) ∂μ) + ε
case intro.intro.intro.intro.intro.refine'_5
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : (∫ (x : α), EReal.toReal (g x) ∂μ) < (∫ (x : α), -f x ∂μ) + ε
⊢ (∫ (x : α), f x ∂μ) < (∫ (x : α), EReal.toReal ((fun x => -g x) x) ∂μ) + ε
simp_rw [integral_neg, lt_neg_add_iff_add_lt] at gint
case intro.intro.intro.intro.intro.refine'_5
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ((∫ (x : α), EReal.toReal (g x) ∂μ) + ∫ (a : α), f a ∂μ) < ε
⊢ (∫ (x : α), f x ∂μ) < (∫ (x : α), EReal.toReal ((fun x => -g x) x) ∂μ) + ε
case intro.intro.intro.intro.intro.refine'_5
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ((∫ (a : α), f a ∂μ) + ∫ (x : α), EReal.toReal (g x) ∂μ) < ε
⊢ (∫ (x : α), f x ∂μ) < (∫ (x : α), EReal.toReal ((fun x => -g x) x) ∂μ) + ε
rw [add_comm] at gint
no goals
case intro.intro.intro.intro.intro.refine'_5
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : WeaklyRegular μ
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable fun x => EReal.toReal (g x)
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ((∫ (x : α), EReal.toReal (g x) ∂μ) + ∫ (a : α), f a ∂μ) < ε
⊢ (∫ (x : α), f x ∂μ) < (∫ (x : α), EReal.toReal ((fun x => -g x) x) ∂μ) + ε
simpa [integral_neg] using gint