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 : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ = ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ

Tactic:
exact lintegral_congr_ae (fmeas.ae_eq_mk.fun_comp _)

Premises used: MeasureTheory.lintegral_congr_ae, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.fun_comp
-- 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 : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
⊢ ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2

Tactic:
g1_int
-- 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 : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
h : 0 = ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ
⊢ ∫⁻ (x : α), g1 x ∂μ ≤ 0 + ε / 2

Tactic:
convert! g1_int
-- 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 : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
⊢ 0 = ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ

Tactic:
simp only [smeas, μs, lintegral_const, Set.univ_inter, MeasurableSet.univ,
            lintegral_indicator, mul_zero, restrict_apply]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply, Set.univ_inter, MulZeroClass.mul_zero, MeasureTheory.lintegral_indicator, MeasurableSet.univ
-- 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 : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + (0 + ε / 2) = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε

Tactic:
simp only [add_assoc, ENNReal.add_halves, zero_add]

Premises used: add_assoc, zero_add, ENNReal.add_halves
-- 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 : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
g0₁ : ∫⁻ (x : α), g0 x ∂μ + ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + (0 + ε / 2)
g0₂ : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + (0 + ε / 2) = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
⊢ ∫⁻ (x : α), (fun (x : α) ↦ g0 x + g1 x) x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε

Tactic:
calc
      ∫⁻ x, g0 x + g1 x ∂μ = (∫⁻ x, g0 x ∂μ) + ∫⁻ x, g1 x ∂μ :=
        lintegral_add_left g0_cont.measurable _
      _ ≤ (∫⁻ x, f x ∂μ) + ε / 2 + (0 + ε / 2) := by
        refine add_le_add ?_ ?_
        · convert! g0_int using 2
          exact lintegral_congr_ae (fmeas.ae_eq_mk.fun_comp _)
        · convert! g1_int
          simp only [smeas, μs, lintegral_const, Set.univ_inter, MeasurableSet.univ,
            lintegral_indicator, mul_zero, restrict_apply]
      _ = (∫⁻ x, f x ∂μ) + ε := by simp only [add_assoc, ENNReal.add_halves, zero_add]

Premises used: ENNReal.ofNNReal, HDiv.hDiv, MeasureTheory.lintegral_add_left, LowerSemicontinuous.measurable, HAdd.hAdd, OfNat.ofNat, MeasureTheory.lintegral
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ
εpos : 0 < ε
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ (↑(f x) : ℝ).toNNReal) μ

Tactic:
fint.aestronglyMeasurable.real_toNNReal.aemeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.real_toNNReal
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ
εpos : 0 < ε
h : ∀ (x : α), f x = (↑(f x) : ℝ).toNNReal
⊢ AEMeasurable f μ

Tactic:
convert! fint.aestronglyMeasurable.real_toNNReal.aemeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.real_toNNReal
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ
εpos : 0 < ε
x : α
⊢ f x = (↑(f x) : ℝ).toNNReal

Tactic:
simp only [Real.toNNReal_coe]

Premises used: Real.toNNReal_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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ
εpos : 0 < ε
⊢ AEMeasurable f μ

Tactic:
have fmeas : AEMeasurable f μ := by
    convert! fint.aestronglyMeasurable.real_toNNReal.aemeasurable
    simp only [Real.toNNReal_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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ
εpos : 0 < ε
fmeas : AEMeasurable f μ
⊢ 0 ≤ ε

Tactic:
εpos.le

Premises used: LT.lt.le
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ
εpos : 0 < ε
fmeas : AEMeasurable f μ
lift :
  ∀ (ε : ℝ≥0) (εpos : 0 < (↑ε : ℝ)),
    ∃ (g : α → ℝ≥0∞),
      (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
        LowerSemicontinuous g ∧
          (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
            Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
              ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + ε

Tactic:
lift ε to ℝ≥0 using εpos.le

Premises used: LT.lt.le
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
⊢ ∃ (δ : ℝ≥0), 0 < δ ∧ δ < ε

Tactic:
exists_between εpos

Premises used: exists_between
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
obtain :
  ∀ (δ : ℝ≥0) (δpos : 0 < δ) (hδε : δ < ε),
    ∃ (g : α → ℝ≥0∞),
      (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
        LowerSemicontinuous g ∧
          (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
            Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
              ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)

Tactic:
obtain ⟨δ, δpos, hδε⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ δ < ε := exists_between εpos

Premises used: exists_between
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞

Tactic:
have int_f_ne_top : (∫⁻ a : α, f a ∂μ) ≠ ∞ :=
    (hasFiniteIntegral_iff_ofNNReal.1 fint.hasFiniteIntegral).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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
rcases :
  ∀ (g : α → ℝ≥0∞) (f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) (gcont : LowerSemicontinuous g)
    (gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)),
    ∃ (g : α → ℝ≥0∞),
      (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
        LowerSemicontinuous g ∧
          (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
            Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
              ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)

Tactic:
rcases exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable μ f fmeas
      (ENNReal.coe_ne_zero.2 δpos.ne') with
    ⟨g, f_lt_g, gcont, gint⟩

Premises used: Iff.mpr, MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge_of_aemeasurable, ENNReal.coe_ne_zero, 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞) ≠ ∞

Tactic:
simpa
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
⊢ ∫⁻ (x : α), g x ∂μ ≠ ∞

Tactic:
have gint_ne : (∫⁻ x : α, g x ∂μ) ≠ ∞ := ne_top_of_le_ne_top (by simpa) gint
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, g x < ∞

Tactic:
have g_lt_top : ∀ᵐ x : α ∂μ, g x < ∞ := ae_lt_top gcont.measurable gint_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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
h : (fun (a : α) ↦ ENNReal.ofReal (g a).toReal) =ᶠ[ae μ] g
⊢ ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
h : ∀ (a : α) (hx : g a < ∞), ENNReal.ofReal (g a).toReal = g a
⊢ (fun (a : α) ↦ ENNReal.ofReal (g a).toReal) =ᶠ[ae μ] g

Tactic:
filter_upwards [g_lt_top] with _ hx
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
a : α
hx : g a < ∞
⊢ ENNReal.ofReal (g a).toReal = g a

Tactic:
simp only [hx.ne, ENNReal.ofReal_toReal, Ne, not_false_iff]

Premises used: ENNReal.ofReal_toReal, Ne, not_false_iff, 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
⊢ ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
have Ig : (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) = ∫⁻ a : α, g a ∂μ := by
    apply lintegral_congr_ae
    filter_upwards [g_lt_top] with _ hx
    simp only [hx.ne, ENNReal.ofReal_toReal, Ne, not_false_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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)

Tactic:
⟨g, f_lt_g, gcont, g_lt_top, ?_, ?_⟩

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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
refine_1 : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
refine_2 : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)

Tactic:
refine ⟨g, f_lt_g, gcont, g_lt_top, ?_, ?_⟩
-- 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ

Tactic:
⟨gcont.measurable.ennreal_toReal.aemeasurable.aestronglyMeasurable, ?_⟩

Premises used: AEMeasurable.aestronglyMeasurable, Measurable.aemeasurable, MeasureTheory.Integrable, LowerSemicontinuous.measurable, And.intro, Measurable.ennreal_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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
refine_1 : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ

Tactic:
refine ⟨gcont.measurable.ennreal_toReal.aemeasurable.aestronglyMeasurable, ?_⟩