awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
x : α
refine_2 : gm x ≤ (-f x).toNNReal
⊢ (↑(↑(gm x) : ℝ≥0∞) : EReal) ≤ (↑(↑(-f x).toNNReal : ℝ≥0∞) : EReal)

Tactic:
simp only [ENNReal.coe_le_coe, EReal.coe_ennreal_le_coe_ennreal_iff]

Premises used: EReal.coe_ennreal_le_coe_ennreal_iff, ENNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
x : α
⊢ gm x ≤ (-f x).toNNReal

Tactic:
gm_le_fm x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
x : α
⊢ gm x ≤ (-f x).toNNReal

Tactic:
exact gm_le_fm x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
x : α
⊢ (↑(↑(gm x) : ℝ≥0∞) : EReal) ≠ ⊥

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
x : α
⊢ (↑(↑(-f x).toNNReal : ℝ≥0∞) : EReal) ≠ ⊤

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
⊢ ∀ (x : α), (↑(f x) : EReal) < g x

Tactic:
case lt =>
    show ∀ x, (f x : EReal) < g x
    intro x
    rw [EReal.coe_real_ereal_eq_coe_toNNReal_sub_coe_toNNReal (f x)]
    refine EReal.sub_lt_sub_of_lt_of_le ?_ ?_ ?_ ?_
    · simp only [EReal.coe_ennreal_lt_coe_ennreal_iff]; exact fp_lt_gp x
    · simp only [ENNReal.coe_le_coe, EReal.coe_ennreal_le_coe_ennreal_iff]
      exact gm_le_fm x
    · simp
    · simp

Premises used: EReal.coe_ennreal_le_coe_ennreal_iff, EReal.sub_lt_sub_of_lt_of_le, ENNReal.coe_le_coe, EReal.coe_ennreal_lt_coe_ennreal_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
hf₁ : LowerSemicontinuous (β := EReal) fun (z : α) ↦ (↑(gp z) : EReal)
hg : LowerSemicontinuous (β := EReal) fun (z : α) ↦ -(↑(↑(gm z) : ℝ≥0∞) : EReal)
hcont :
  ∀ (x : α),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑(gp x) : EReal), -(↑(↑(gm x) : ℝ≥0∞) : EReal))
⊢ LowerSemicontinuous g

Tactic:
apply LowerSemicontinuous.add'

Premises used: LowerSemicontinuous.add'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
⊢ LowerSemicontinuous (β := EReal) fun (z : α) ↦ (↑(gp z) : EReal)

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

Premises used: Iff.mpr, EReal.coe_ennreal_le_coe_ennreal_iff, Continuous.comp_lowerSemicontinuous, continuous_coe_ennreal_ereal, ENNReal.toEReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
⊢ LowerSemicontinuous (β := EReal) fun (z : α) ↦ (↑(gp z) : EReal)

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

Premises used: Iff.mpr, EReal.coe_ennreal_le_coe_ennreal_iff, Continuous.comp_lowerSemicontinuous, continuous_coe_ennreal_ereal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
apply : UpperSemicontinuous (β := EReal) fun (z : α) ↦ (↑(↑(gm z) : ℝ≥0∞) : EReal)
⊢ LowerSemicontinuous (β := EReal) fun (z : α) ↦ -(↑(↑(gm z) : ℝ≥0∞) : EReal)

Tactic:
apply continuous_neg.comp_upperSemicontinuous_antitone _ fun x y hxy =>
          EReal.neg_le_neg_iff.2 hxy

Premises used: Iff.mpr, ContinuousNeg.continuous_neg, EReal.neg_le_neg_iff, Continuous.comp_upperSemicontinuous_antitone
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
apply : UpperSemicontinuous (β := ℝ≥0∞) fun (z : α) ↦ (↑(gm z) : ℝ≥0∞)
⊢ UpperSemicontinuous (β := EReal) fun (z : α) ↦ (↑(↑(gm z) : ℝ≥0∞) : EReal)

Tactic:
apply continuous_coe_ennreal_ereal.comp_upperSemicontinuous _ fun x y hxy =>
          EReal.coe_ennreal_le_coe_ennreal_iff.2 hxy

Premises used: Iff.mpr, EReal.coe_ennreal_le_coe_ennreal_iff, Continuous.comp_upperSemicontinuous, continuous_coe_ennreal_ereal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
⊢ UpperSemicontinuous (β := ℝ≥0∞) fun (z : α) ↦ (↑(gm z) : ℝ≥0∞)

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

Premises used: Iff.mpr, ENNReal.ofNNReal, ENNReal.coe_le_coe, Continuous.comp_upperSemicontinuous, WithTop.some, ENNReal.continuous_coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
⊢ UpperSemicontinuous (β := ℝ≥0∞) fun (z : α) ↦ (↑(gm z) : ℝ≥0∞)

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

Premises used: Iff.mpr, ENNReal.coe_le_coe, Continuous.comp_upperSemicontinuous, ENNReal.continuous_coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
x : α
⊢ ((↑(gp x) : EReal), -(↑(↑(gm x) : ℝ≥0∞) : EReal)).1 ≠ ⊤ ∨ ((↑(gp x) : EReal), -(↑(↑(gm x) : ℝ≥0∞) : EReal)).2 ≠ ⊥

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
x : α
⊢ ((↑(gp x) : EReal), -(↑(↑(gm x) : ℝ≥0∞) : EReal)).1 ≠ ⊥ ∨ ((↑(gp x) : EReal), -(↑(↑(gm x) : ℝ≥0∞) : EReal)).2 ≠ ⊤

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 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) : ℝ≥0∞) < 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) : ℝ) ∂μ + (↑δ : ℝ)
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) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
x : α
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑(gp x) : EReal), -(↑(↑(gm x) : ℝ≥0∞) : EReal))

Tactic:
exact EReal.continuousAt_add (by simp) (by simp)

Premises used: EReal.continuousAt_add