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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
n : ℕ
⊢ LowerSemicontinuous (β := ℝ≥0∞) fun (x : α) ↦ (↑(g n x) : ℝ≥0∞)

Tactic:
ENNReal.continuous_coe.comp_lowerSemicontinuous (gcont n) fun x y hxy =>
        ENNReal.coe_le_coe.2 hxy

Premises used: Iff.mpr, ENNReal.ofNNReal, Continuous.comp_lowerSemicontinuous, ENNReal.coe_le_coe, 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
n : ℕ
⊢ LowerSemicontinuous (β := ℝ≥0∞) fun (x : α) ↦ (↑(g n x) : ℝ≥0∞)

Tactic:
exact
      ENNReal.continuous_coe.comp_lowerSemicontinuous (gcont n) fun x y hxy =>
        ENNReal.coe_le_coe.2 hxy

Premises used: Iff.mpr, Continuous.comp_lowerSemicontinuous, ENNReal.coe_le_coe, 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
rw rw₁ : Eq (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (a : α), (↑(g i a) : ℝ≥0∞) ∂μ) (∑' (n : ℕ), ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ)
⊢ ∫⁻ (x : α), ∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) ∂μ = ∑' (n : ℕ), ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ

Tactic:
rw [lintegral_tsum fun n => (gcont n).measurable.coe_nnreal_ennreal.aemeasurable]

Premises used: Measurable.aemeasurable, Measurable.coe_nnreal_ennreal, LowerSemicontinuous.measurable, MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ)
    (∑' (n : ℕ), (∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n))

Tactic:
ENNReal.tsum_le_tsum hg

Premises used: ENNReal.tsum_le_tsum
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ ∑' (n : ℕ), (∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ)
      (∑' (n : ℕ), δ n)

Tactic:
ENNReal.tsum_add

Premises used: ENNReal.tsum_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ)
      (∑' (n : ℕ), δ n) ≤
    ∫⁻ (x : α), f x ∂μ + ε

Tactic:
add_le_add ?_ hδ.le

Premises used: add_le_add, 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
refine : ∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ)
      (∑' (n : ℕ), δ n) ≤
    ∫⁻ (x : α), f x ∂μ + ε

Tactic:
refine add_le_add ?_ hδ.le

Premises used: add_le_add, 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
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
rw : ∫⁻ (a : α), ∑' (i : ℕ), (↑(((eapproxDiff f i : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), f x ∂μ
rw₁ : ∀ (i : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(((eapproxDiff f i : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞)) μ
⊢ ∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
rw [← lintegral_tsum]

Premises used: MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
simp_rw : ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), f a ∂μ
⊢ ∫⁻ (a : α), ∑' (i : ℕ), (↑(((eapproxDiff f i : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
simp_rw [tsum_eapproxDiff f hf, le_refl]

Premises used: le_refl, MeasureTheory.SimpleFunc.tsum_eapproxDiff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
n : ℕ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞)) μ

Tactic:
(SimpleFunc.measurable _).coe_nnreal_ennreal.aemeasurable

Premises used: Measurable.aemeasurable, Measurable.coe_nnreal_ennreal, MeasureTheory.SimpleFunc.measurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
n : ℕ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞)) μ

Tactic:
exact (SimpleFunc.measurable _).coe_nnreal_ennreal.aemeasurable

Premises used: Measurable.aemeasurable, Measurable.coe_nnreal_ennreal, MeasureTheory.SimpleFunc.measurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : (n : ℕ) → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), ((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg :
  ∀ (n : ℕ),
    ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + δ n
n : ∫⁻ (x : α), ∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) ∂μ = ∑' (n : ℕ), ∫⁻ (x : α), (↑(g n x) : ℝ≥0∞) ∂μ
n₁ :
  HAdd.hAdd (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : α), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ)
      (∑' (n : ℕ), δ n) ≤
    ∫⁻ (x : α), f x ∂μ + ε
⊢ ∫⁻ (x : α), (fun (x : α) ↦ (∑' (n : ℕ), (↑(g n x) : ℝ≥0∞) : ℝ≥0∞)) x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε

Tactic:
calc
      ∫⁻ x, ∑' n : ℕ, g n x ∂μ = ∑' n, ∫⁻ x, g n x ∂μ := by
        rw [lintegral_tsum fun n => (gcont n).measurable.coe_nnreal_ennreal.aemeasurable]
      _ ≤ ∑' n, ((∫⁻ x, eapproxDiff f n x ∂μ) + δ n) := ENNReal.tsum_le_tsum hg
      _ = ∑' n, ∫⁻ x, eapproxDiff f n x ∂μ + ∑' n, δ n := ENNReal.tsum_add
      _ ≤ (∫⁻ x : α, f x ∂μ) + ε := by
        refine add_le_add ?_ hδ.le
        rw [← lintegral_tsum]
        · simp_rw [tsum_eapproxDiff f hf, le_refl]
        · intro n; exact (SimpleFunc.measurable _).coe_nnreal_ennreal.aemeasurable

Premises used: ENNReal.tsum_le_tsum, ENNReal.tsum_add, 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
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ε / 2 ≠ 0

Tactic:
have : ε / 2 ≠ 0 := (ENNReal.half_pos ε0).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
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
rcases :
  ∀ (w : α → ℝ≥0) (wpos : ∀ (x : α), 0 < w x) (wmeas : Measurable w) (wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2),
    ∃ (g : α → ℝ≥0∞),
      (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε

Tactic:
rcases exists_pos_lintegral_lt_of_sigmaFinite μ this with ⟨w, wpos, wmeas, wint⟩

Premises used: MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite
-- 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 : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
rcases :
  ∀ (g : α → ℝ≥0∞) (le_g : ∀ (x : α), f' x ≤ g x) (gcont : LowerSemicontinuous g)
    (gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2),
    ∃ (g : α → ℝ≥0∞),
      (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧
        LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε

Tactic:
rcases exists_le_lowerSemicontinuous_lintegral_ge μ f' (fmeas.add wmeas).coe_nnreal_ennreal
      this with
    ⟨g, le_g, gcont, gint⟩

Premises used: MeasureTheory.exists_le_lowerSemicontinuous_lintegral_ge, Measurable.coe_nnreal_ennreal, Measurable.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 : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε

Tactic:
⟨g, fun x => ?_, gcont, ?_⟩

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
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
refine_1 : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
refine_2 : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε

Tactic:
refine ⟨g, fun x => ?_, gcont, ?_⟩
-- 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 : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
x : α
⊢ (↑(f x) : ℝ≥0∞) < f' x

Tactic:
simpa only [← ENNReal.coe_lt_coe, add_zero] using add_lt_add_right (wpos x) (f x)

Premises used: add_lt_add_right, ENNReal.coe_lt_coe, add_zero
-- 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 : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
x : α
⊢ f' x ≤ g x

Tactic:
le_g 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 : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
x : α
x₁ : (↑(f x) : ℝ≥0∞) < f' x
⊢ (↑(f x) : ℝ≥0∞) < g x

Tactic:
calc
      (f x : ℝ≥0∞) < f' x := by
        simpa only [← ENNReal.coe_lt_coe, add_zero] using add_lt_add_right (wpos x) (f x)
      _ ≤ g x := le_g x

Premises used: ENNReal.ofNNReal
-- 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 : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) + (↑(w x) : ℝ≥0∞) ∂μ + ε / 2

Tactic:
gint

Premises used: ENNReal.ofNNReal, WithTop.map₂, WithTop.some, Option.map₂
-- 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 : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
rw rw₁ :
  ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(w a) : ℝ≥0∞) ∂μ + ε / 2 =
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) + (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 =
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2

Tactic:
rw [lintegral_add_right _ wmeas.coe_nnreal_ennreal]

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.lintegral_add_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 : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
grw grw₁ : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2 ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 ≤
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2

Tactic:
grw [wint]
-- 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 : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
rw : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2) = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
rw₁ rw₂ : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2 = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε

Tactic:
rw [add_assoc, ENNReal.add_halves]

Premises used: add_assoc, 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 : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
x :
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) + (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 =
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2
x₁ :
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 ≤
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2
x₂ : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2 = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε

Tactic:
calc
      (∫⁻ x : α, g x ∂μ) ≤ (∫⁻ x : α, f x + w x ∂μ) + ε / 2 := gint
      _ = ((∫⁻ x : α, f x ∂μ) + ∫⁻ x : α, w x ∂μ) + ε / 2 := by
        rw [lintegral_add_right _ wmeas.coe_nnreal_ennreal]
      _ ≤ (∫⁻ x : α, f x ∂μ) + ε / 2 + ε / 2 := by grw [wint]
      _ = (∫⁻ x : α, f x ∂μ) + ε := by rw [add_assoc, ENNReal.add_halves]

Premises used: ENNReal.ofNNReal, HAdd.hAdd, 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
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ε / 2 ≠ 0

Tactic:
have : ε / 2 ≠ 0 := (ENNReal.half_pos ε0).ne'