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₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ (f₂ : (a : α) → ℝ≥0) x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2
add :
  ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fun (x : α) ↦ g₁ x + g₂ x) x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (f₁ + f₂ : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε

Tactic:
refine
      ⟨fun x => g₁ x + g₂ x, fun x => add_le_add (f₁_le_g₁ x) (f₂_le_g₂ x), g₁cont.add g₂cont, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ (f₂ : (a : α) → ℝ≥0) x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2
add :
  ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) + (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) + (↑(g₂ x) : ℝ≥0∞) ∂μ + ε
⊢ ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fun (x : α) ↦ g₁ x + g₂ x) x) : ℝ≥0∞) ∂μ + ε

Tactic:
simp only [SimpleFunc.coe_add, ENNReal.coe_add, Pi.add_apply]

Premises used: MeasureTheory.SimpleFunc.coe_add, ENNReal.coe_add, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ (f₂ : (a : α) → ℝ≥0) x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2
add :
  ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + ε
⊢ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) + (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) + (↑(g₂ x) : ℝ≥0∞) ∂μ + ε

Tactic:
rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal,
      lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal]

Premises used: UpperSemicontinuous.measurable, Measurable.coe_nnreal_ennreal, MeasureTheory.SimpleFunc.measurable, MeasureTheory.lintegral_add_left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ (f₂ : (a : α) → ℝ≥0) x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2 + (∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2)

Tactic:
add_le_add g₁int g₂int

Premises used: add_le_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h_1 :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ (f₂ : (a : α) → ℝ≥0) x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2
h :
  ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + ε =
    ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2 + (∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2)
⊢ ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + ε

Tactic:
convert! add_le_add g₁int g₂int using 1

Premises used: add_le_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ (f₂ : (a : α) → ℝ≥0) x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2
rw : ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2)
| ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + ε

Tactic:
rw [← ENNReal.add_halves ε]

Premises used: 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
f₁ f₂ : α →ₛ ℝ≥0
h_1 :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ (f₂ : (a : α) → ℝ≥0) x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2
h :
  ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2) =
    ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2 + (∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2)
⊢ ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + ε =
    ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2 + (∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2)

Tactic:
conv_lhs => rw [← ENNReal.add_halves ε]

Premises used: 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
f₁ f₂ : α →ₛ ℝ≥0
h :
  Disjoint (α := Set α) (Function.support (M := ℝ≥0) (⇑f₁ : (a : α) → ℝ≥0))
    (Function.support (M := ℝ≥0) (⇑f₂ : (a : α) → ℝ≥0))
h₁ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₁ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
h₂ :
  ∀ (int_f : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞) {ε : ℝ≥0∞} (ε0 : ε ≠ 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (f₂ : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
int_f : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
A : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g₁ : α → ℝ≥0
f₁_le_g₁ : ∀ (x : α), g₁ x ≤ (f₁ : (a : α) → ℝ≥0) x
g₁cont : UpperSemicontinuous g₁
g₁int : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2
g₂ : α → ℝ≥0
f₂_le_g₂ : ∀ (x : α), g₂ x ≤ (f₂ : (a : α) → ℝ≥0) x
g₂cont : UpperSemicontinuous g₂
g₂int : ∫⁻ (x : α), (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2) =
    ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2 + (∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2

Tactic:
have := ENNReal.lt_add_right int_f (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
f : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2
rw :
  (⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
        (SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ) +
    ε / 2
| ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2

Tactic:
rw [lintegral_eq_nnreal (fun x => (f x : ℝ≥0∞)) μ]

Premises used: ENNReal.ofNNReal, MeasureTheory.lintegral_eq_nnreal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ <
    (⨆ (φ : α →ₛ ℝ≥0),
        ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
          (SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ) +
      ε / 2

Tactic:
conv_rhs at this => rw [lintegral_eq_nnreal (fun x => (f x : ℝ≥0∞)) μ]

Premises used: ENNReal.ofNNReal, MeasureTheory.lintegral_eq_nnreal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
this :
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ <
    (⨆ (φ : α →ₛ ℝ≥0),
        ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
          (SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ) +
      ε / 2
rw :
  ∀
    (this :
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ <
        ⨆ (i : α →ₛ ℝ≥0),
          ⨆ (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
            (SimpleFunc.map ENNReal.ofNNReal i).lintegral μ + ε / 2),
    ∃ (fs : α →ₛ ℝ≥0),
      (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
        ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
h : ∃ (i : α →ₛ ℝ≥0), ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
⊢ ∃ (fs : α →ₛ ℝ≥0),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2

Tactic:
rw [ENNReal.biSup_add'] at this

Premises used: ENNReal.biSup_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
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
this :
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ <
    (⨆ (φ : α →ₛ ℝ≥0),
        ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
          (SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ) +
      ε / 2
x : α
⊢ (↑(((0 : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
this :
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ <
    (⨆ (φ : α →ₛ ℝ≥0),
        ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
          (SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ) +
      ε / 2
⊢ ∃ (i : α →ₛ ℝ≥0), ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)

Tactic:
exact ⟨0, fun x => by simp⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
this :
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ <
    (⨆ (φ : α →ₛ ℝ≥0),
        ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
          (SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ) +
      ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ <
    ⨆ (i : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
        (SimpleFunc.map ENNReal.ofNNReal i).lintegral μ + ε / 2

Tactic:
rw [ENNReal.biSup_add'] at this <;> [skip; exact ⟨0, fun x => by simp⟩]

Premises used: ENNReal.biSup_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
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
this :
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ <
    ⨆ (i : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
        (SimpleFunc.map ENNReal.ofNNReal i).lintegral μ + ε / 2
⊢ ∃ (i : α →ₛ ℝ≥0) (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < (SimpleFunc.map ENNReal.ofNNReal i).lintegral μ + ε / 2

Tactic:
simp only [lt_iSup_iff] at this

Premises used: lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
this :
  ∃ (i : α →ₛ ℝ≥0) (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < (SimpleFunc.map ENNReal.ofNNReal i).lintegral μ + ε / 2
rcases :
  ∀ (fs : α →ₛ ℝ≥0) (fs_le_f : ∀ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞))
    (int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < (SimpleFunc.map ENNReal.ofNNReal fs).lintegral μ + ε / 2),
    ∃ (fs : α →ₛ ℝ≥0),
      (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
        ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∃ (fs : α →ₛ ℝ≥0),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2

Tactic:
rcases this with ⟨fs, fs_le_f, int_fs⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < (SimpleFunc.map ENNReal.ofNNReal fs).lintegral μ + ε / 2
x : α
⊢ (fs : (a : α) → ℝ≥0) x ≤ f x

Tactic:
simpa only [ENNReal.coe_le_coe] using fs_le_f x

Premises used: 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
f : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < (SimpleFunc.map ENNReal.ofNNReal fs).lintegral μ + ε / 2
refine : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∃ (fs : α →ₛ ℝ≥0),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2

Tactic:
refine ⟨fs, fun x => by simpa only [ENNReal.coe_le_coe] using fs_le_f x, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < (SimpleFunc.map ENNReal.ofNNReal fs).lintegral μ + ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ (SimpleFunc.map ENNReal.ofNNReal fs).lintegral μ + ε / 2

Tactic:
int_fs.le

Premises used: LT.lt.le