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 : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have obtain : ∀ (fs : α →ₛ ℝ≥0) (fs_le_f : ∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x)
  (int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: obtain ⟨fs, fs_le_f, int_fs⟩ :
    ∃ fs : α →ₛ ℝ≥0, (∀ x, fs x ≤ f x) ∧ (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, fs x ∂μ) + ε / 2 := by
    have := ENNReal.lt_add_right int_f (ENNReal.half_pos ε0).ne'
    conv_rhs at this => rw [lintegral_eq_nnreal (fun x => (f x : ℝ≥0∞)) μ]
    rw [ENNReal.biSup_add'] at this <;> [skip; exact ⟨0, fun x => by simp⟩]
    simp only [lt_iSup_iff] at this
    rcases this with ⟨fs, fs_le_f, int_fs⟩
    refine ⟨fs, fun x => by simpa only [ENNReal.coe_le_coe] using fs_le_f x, ?_⟩
    convert! int_fs.le
    rw [← SimpleFunc.lintegral_eq_lintegral]
    simp only [SimpleFunc.coe_map, Function.comp_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 : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x
int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
have refine : ∀ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
Tactic: refine ne_top_of_le_ne_top int_f (lintegral_mono fun x => ?_)
-- 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
fs_le_f : ∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x
int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have int_fs_lt_top : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
Tactic: have int_fs_lt_top : (∫⁻ x, fs x ∂μ) ≠ ∞ := by
    refine ne_top_of_le_ne_top int_f (lintegral_mono fun x => ?_)
    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 ≤ f x
int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
int_fs_lt_top : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have obtain : ∀ (g : α → ℝ≥0) (g_le_fs : ∀ (x : α), g x ≤ (fs : (a : α) → ℝ≥0) x) (gcont : UpperSemicontinuous g)
  (gint : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε / 2),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: obtain ⟨g, g_le_fs, gcont, gint⟩ :
    ∃ g : α → ℝ≥0,
      (∀ x, g x ≤ fs x) ∧ UpperSemicontinuous g ∧ (∫⁻ x, fs x ∂μ) ≤ (∫⁻ x, g x ∂μ) + ε / 2 :=
    fs.exists_upperSemicontinuous_le_lintegral_le int_fs_lt_top (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
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x
int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
int_fs_lt_top : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ (fs : (a : α) → ℝ≥0) x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have refine : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: refine ⟨g, fun x => (g_le_fs x).trans (fs_le_f x), gcont, ?_⟩
-- 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 ≤ f x
int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
int_fs_lt_top : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ (fs : (a : α) → ℝ≥0) x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2 = ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have rw : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2) = ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: rw [add_assoc, 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 : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x
int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
int_fs_lt_top : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ (fs : (a : α) → ℝ≥0) x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε / 2
rw : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2) = ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
⊢ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2 = ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have rw₁ : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε = ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: rw [add_assoc, 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 : α → ℝ≥0
int_f : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
fs : α →ₛ ℝ≥0
fs_le_f : ∀ (x : α), (fs : (a : α) → ℝ≥0) x ≤ f x
int_fs : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ + ε / 2
int_fs_lt_top : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0
g_le_fs : ∀ (x : α), g x ≤ (fs : (a : α) → ℝ≥0) x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑((fs : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have f₁ : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2 = ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: calc
    (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, fs x ∂μ) + ε / 2 := int_fs
    _ ≤ (∫⁻ x, g x ∂μ) + ε / 2 + ε / 2 := add_le_add gint le_rfl
    _ = (∫⁻ x, g x ∂μ) + ε := by rw [add_assoc, 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 : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ
εpos : 0 < ε
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ ∧ ∫ (x : α), (↑(f x) : ℝ) ∂μ - ε ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have lift : ∀ (ε : ℝ≥0) (εpos : 0 < (↑ε : ℝ)),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ ∧
          ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
Tactic: lift ε to ℝ≥0 using εpos.le
Cleared hypotheses: ε, εpos
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ ∧
          ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have εpos₁ : 0 < (↑ε : ℝ≥0∞)
Tactic: rw [NNReal.coe_pos, ← ENNReal.coe_pos] at εpos
Cleared hypotheses: εpos
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ ∧
          ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
Tactic: have If : (∫⁻ x, f x ∂μ) < ∞ := hasFiniteIntegral_iff_ofNNReal.1 fint.hasFiniteIntegral
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ ∧
          ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have rcases : ∀ (g : α → ℝ≥0) (gf : ∀ (x : α), g x ≤ f x) (gcont : UpperSemicontinuous g)
  (gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ ∧
          ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
Tactic: rcases exists_upperSemicontinuous_le_lintegral_le f If.ne εpos.ne' with ⟨g, gf, gcont, gint⟩
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
⊢ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
have refine : ∀ (x : α), (↑(g x) : ℝ≥0∞) ≤ (↑(f x) : ℝ≥0∞)
Tactic: refine lt_of_le_of_lt (lintegral_mono fun x => ?_) If
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ ∧
          ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
Tactic: have Ig : (∫⁻ x, g x ∂μ) < ∞ := by
    refine lt_of_le_of_lt (lintegral_mono fun x => ?_) If
    simpa using gf 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ ∧
          ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have refine_1 : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ
Tactic: refine ⟨g, gf, gcont, ?_, ?_⟩
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
refine_1 : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ f x) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ ∧
          ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have refine_2 : ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
Tactic: refine ⟨g, gf, gcont, ?_, ?_⟩
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ
have refine_1 : ∀ᵐ (a : α) ∂μ, ‖(↑(g a) : ℝ)‖ ≤ ‖(↑(f a) : ℝ)‖
Tactic: refine
      Integrable.mono fint gcont.measurable.coe_nnreal_real.aemeasurable.aestronglyMeasurable ?_
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
⊢ ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have refine_2 : (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal - (↑ε : ℝ) ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
refine_2 :
  (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal - (↑ε : ℝ) ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal
⊢ ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have refine_2₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(g x) : ℝ)
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
refine_2 :
  (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal - (↑ε : ℝ) ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal
refine_2₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(g x) : ℝ)
⊢ ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have refine_2₂ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
refine_2 :
  (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal - (↑ε : ℝ) ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal
refine_2₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(g x) : ℝ)
refine_2₂ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ
⊢ ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have refine_2₃ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(f x) : ℝ)
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
refine_2 :
  (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal - (↑ε : ℝ) ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal
refine_2₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(g x) : ℝ)
refine_2₂ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ
refine_2₃ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(f x) : ℝ)
⊢ ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ
have refine_2₄ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
⊢ (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal - (↑ε : ℝ) ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal
have refine_2 : (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
Tactic: rw [sub_le_iff_le_add]
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
⊢ (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
have h : ∀ (x : α), ENNReal.ofReal (↑(f x) : ℝ) = (↑(f x) : ℝ≥0∞)
Tactic: convert! ENNReal.toReal_mono _ gint
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
h : ∀ (x : α), ENNReal.ofReal (↑(f x) : ℝ) = (↑(f x) : ℝ≥0∞)
⊢ (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
have h₁ : (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ) = (∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)).toReal
Tactic: convert! ENNReal.toReal_mono _ gint
-- 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
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
h : ∀ (x : α), ENNReal.ofReal (↑(f x) : ℝ) = (↑(f x) : ℝ≥0∞)
h₁ :
  (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ) = (∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)).toReal
⊢ (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
have refine_2 : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞) ≠ ∞
Tactic: convert! ENNReal.toReal_mono _ gint