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)
a : α
hx : gp a < ∞
⊢ (↑(↑(gm a) : ℝ≥0∞) : EReal) ≠ ⊥

Tactic:
simp [hx.ne]

Premises used: LT.lt.ne
-- 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)
⊢ ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal

Tactic:
have ae_g : ∀ᵐ x ∂μ, (g x).toReal = (gp x : EReal).toReal - (gm x : EReal).toReal := by
    filter_upwards [gp_lt_top] with _ hx
    rw [EReal.toReal_sub] <;> simp [hx.ne]
-- 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
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε

Tactic:
⟨g, ?lt, ?lsc, ?int, ?aelt, ?intlt⟩

Premises used: And.intro, Exists.intro
-- 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
refine : ∀ (x : α), (↑(f x) : EReal) < g x
refine₁ : LowerSemicontinuous g
refine₂ : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
refine₃ : ∀ᵐ (x : α) ∂μ, g x < ⊤
refine₄ : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε

Tactic:
refine ⟨g, ?lt, ?lsc, ?int, ?aelt, ?intlt⟩
-- 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
rw : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ

Tactic:
rw [integrable_congr ae_g]

Premises used: MeasureTheory.integrable_congr
-- 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
⊢ Integrable (HSub.hSub (α := α → ℝ) (fun (x : α) ↦ (gp x).toReal) fun (x : α) ↦ (↑(gm x) : ℝ)) μ

Tactic:
gp_integrable.sub gm_integrable

Premises used: MeasureTheory.Integrable.sub
-- 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
h :
  ∀ (x : α),
    (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal =
      HSub.hSub (α := α → ℝ) (β := α → ℝ) (fun (x : α) ↦ (gp x).toReal) (fun (x : α) ↦ (↑(gm x) : ℝ)) x
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal) μ

Tactic:
convert! gp_integrable.sub gm_integrable

Premises used: MeasureTheory.Integrable.sub
-- 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).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal =
    HSub.hSub (α := α → ℝ) (β := α → ℝ) (fun (x : α) ↦ (gp x).toReal) (fun (x : α) ↦ (↑(gm x) : ℝ)) x

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
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ

Tactic:
case int =>
    show Integrable (fun x => EReal.toReal (g x)) μ
    rw [integrable_congr ae_g]
    convert! gp_integrable.sub gm_integrable
    simp

Premises used: MeasureTheory.integrable_congr, MeasureTheory.Integrable, MeasureTheory.Integrable.sub, EReal.toReal
-- 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
simp :
  ∫ (x : α), (gp x).toReal - (↑(gm x) : ℝ) ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : α), (gp x).toReal ∂μ) (∫ (x : α), (↑(gm x) : ℝ) ∂μ)
⊢ ∫ (x : α), (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : α), (↑(gp x) : EReal).toReal ∂μ) (∫ (x : α), (↑(gm x) : ℝ) ∂μ)

Tactic:
simp only [EReal.toReal_coe_ennreal, ENNReal.coe_toReal]

Premises used: ENNReal.coe_toReal, EReal.toReal_coe_ennreal
-- 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).toReal - (↑(gm x) : ℝ) ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : α), (gp x).toReal ∂μ) (∫ (x : α), (↑(gm x) : ℝ) ∂μ)

Tactic:
integral_sub gp_integrable gm_integrable

Premises used: MeasureTheory.integral_sub
-- 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).toReal - (↑(gm x) : ℝ) ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : α), (gp x).toReal ∂μ) (∫ (x : α), (↑(gm x) : ℝ) ∂μ)

Tactic:
exact integral_sub gp_integrable gm_integrable

Premises used: MeasureTheory.integral_sub
-- 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
h : ∫ (x : α), (↑(gp x) : EReal).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
⊢ HSub.hSub (α := ℝ) (∫ (x : α), (↑(gp x) : EReal).toReal ∂μ) (∫ (x : α), (↑(gm x) : ℝ) ∂μ) <
    ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ) - ∫ (x : α), (↑(gm x) : ℝ) ∂μ

Tactic:
apply sub_lt_sub_right

Premises used: sub_lt_sub_right
-- 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).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)

Tactic:
gpint
-- 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
h : ∀ (x : α), (↑(gp x) : EReal).toReal = (gp x).toReal
⊢ ∫ (x : α), (↑(gp x) : EReal).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)

Tactic:
convert! gpint
-- 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).toReal = (gp x).toReal

Tactic:
simp only [EReal.toReal_coe_ennreal]

Premises used: EReal.toReal_coe_ennreal