awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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),
    (∀ (x : α), g x ≤ (f₁ + f₂ : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have add : ∀ (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),
    (∀ (x : α), g x ≤ (f₁ + f₂ : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: rcases h₂ (ENNReal.add_ne_top.1 A).2 (ENNReal.half_pos ε0).ne' with
      ⟨g₂, f₂_le_g₂, g₂cont, g₂int⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (f₁ + f₂ : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have add : ∫⁻ (x : α), (↑((f₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fun (x : α) ↦ g₁ x + g₂ x) 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, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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₁ + f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fun (x : α) ↦ g₁ x + g₂ x) x) : ℝ≥0∞) ∂μ + ε
have add : ∫⁻ (x : α), (↑((f₁ : (a : α) → ℝ≥0) x) : ℝ≥0∞) + (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
  ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) + (↑(g₂ x) : ℝ≥0∞) ∂μ + ε
Tactic: simp only [SimpleFunc.coe_add, ENNReal.coe_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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∞) + (↑((f₂ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) + (↑(g₂ x) : ℝ≥0∞) ∂μ + ε
have add : ∫⁻ (a : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤
  ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + ε
Tactic: rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal,
      lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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 : α), (↑((f₁ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑((f₂ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤
    ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + ε
have h : ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + ε =
  ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2 + (∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2)
Tactic: convert! add_le_add g₁int g₂int using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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∞) ∂μ + ε
have rw : ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2)
Tactic: rw [← ENNReal.add_halves ε]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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∞) ∂μ + ε =
    ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2 + (∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2)
have h : ∫⁻ (a : α), (↑(g₁ a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(g₂ a) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2) =
  ∫⁻ (x : α), (↑(g₁ x) : ℝ≥0∞) ∂μ + ε / 2 + (∫⁻ (x : α), (↑(g₂ x) : ℝ≥0∞) ∂μ + ε / 2)
Tactic: conv_lhs => rw [← ENNReal.add_halves ε]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
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),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
have this : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2
Tactic: have := ENNReal.lt_add_right int_f (ENNReal.half_pos ε0).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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∞) ∂μ + ε / 2
have rw : (⨆ (φ : α →ₛ ℝ≥0),
    ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)),
      (SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ) +
  ε / 2
Tactic: rw [lintegral_eq_nnreal (fun x => (f x : ℝ≥0∞)) μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
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
⊢ ∃ (fs : α →ₛ ℝ≥0),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
have this₁ : ∫⁻ (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∞)) μ]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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
⊢ ∃ (fs : α →ₛ ℝ≥0),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
have 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
Tactic: rw [ENNReal.biSup_add'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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
⊢ ∃ (fs : α →ₛ ℝ≥0),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
have h : ∃ (i : α →ₛ ℝ≥0), ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
Tactic: rw [ENNReal.biSup_add'] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
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
⊢ ∃ (fs : α →ₛ ℝ≥0),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
have this₁ : ∫⁻ (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⟩]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (hypothesis)
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
⊢ ∃ (fs : α →ₛ ℝ≥0),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
have this₁ : ∃ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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
⊢ ∃ (fs : α →ₛ ℝ≥0),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
have 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
Tactic: rcases this with ⟨fs, fs_le_f, int_fs⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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
⊢ ∃ (fs : α →ₛ ℝ≥0),
    (∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x) ∧
      ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
have refine : ∫⁻ (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, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
have h : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ = (SimpleFunc.map ENNReal.ofNNReal fs).lintegral μ
Tactic: convert! int_fs.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (goal)
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) : ℝ≥0∞) ∂μ = (SimpleFunc.map ENNReal.ofNNReal fs).lintegral μ
have h : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ =
  ∫⁻ (a : α), (SimpleFunc.map ENNReal.ofNNReal fs : (a : α) → ℝ≥0∞) a ∂μ
Tactic: rw [← SimpleFunc.lintegral_eq_lintegral]