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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
refine_2 :
  (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
refine_2₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(f x) : ℝ)
⊢ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
refine_2 :
  (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
refine_2₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(f x) : ℝ)
refine_2₂ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
⊢ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have refine_2₃ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (g x).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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
refine_2 :
  (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
refine_2₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(f x) : ℝ)
refine_2₂ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
refine_2₃ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (g x).toReal
⊢ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), (↑(f x) : ℝ) ∂μ + (↑ε : ℝ)
have refine_2₄ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (g x).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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), g a ∂μ).toReal ≤ (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)).toReal
have apply : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞) ≠ ∞
Tactic: apply 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)).toReal = (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ)
have rw : (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ≥0∞).toReal = (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ)
Tactic: rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
-- 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
rw : (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ≥0∞).toReal = (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ)
⊢ (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)).toReal = (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ)
have rw₁ : (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ) = (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ)
Tactic: rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
-- 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
have a : (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal = (∫⁻ (a : α), g a ∂μ).toReal
Tactic: calc
        ENNReal.toReal (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) =
            ENNReal.toReal (∫⁻ a : α, g a ∂μ) := by congr 1
        _ ≤ ENNReal.toReal ((∫⁻ a : α, f a ∂μ) + δ) := by
          apply ENNReal.toReal_mono _ gint
          simpa using int_f_ne_top
        _ = ENNReal.toReal (∫⁻ a : α, f a ∂μ) + δ := by
          rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
        _ < ENNReal.toReal (∫⁻ a : α, f a ∂μ) + ε := by gcongr
        _ = (∫⁻ a : α, ENNReal.ofReal ↑(f a) ∂μ).toReal + ε := by simp
-- 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
a : (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal = (∫⁻ (a : α), g a ∂μ).toReal
⊢ (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
have a₁ : (∫⁻ (a : α), g a ∂μ).toReal ≤ (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)).toReal
Tactic: calc
        ENNReal.toReal (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) =
            ENNReal.toReal (∫⁻ a : α, g a ∂μ) := by congr 1
        _ ≤ ENNReal.toReal ((∫⁻ a : α, f a ∂μ) + δ) := by
          apply ENNReal.toReal_mono _ gint
          simpa using int_f_ne_top
        _ = ENNReal.toReal (∫⁻ a : α, f a ∂μ) + δ := by
          rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
        _ < ENNReal.toReal (∫⁻ a : α, f a ∂μ) + ε := by gcongr
        _ = (∫⁻ a : α, ENNReal.ofReal ↑(f a) ∂μ).toReal + ε := by simp
-- 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
a : (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal = (∫⁻ (a : α), g a ∂μ).toReal
a₁ : (∫⁻ (a : α), g a ∂μ).toReal ≤ (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)).toReal
⊢ (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
have a₂ : (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)).toReal = (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ)
Tactic: calc
        ENNReal.toReal (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) =
            ENNReal.toReal (∫⁻ a : α, g a ∂μ) := by congr 1
        _ ≤ ENNReal.toReal ((∫⁻ a : α, f a ∂μ) + δ) := by
          apply ENNReal.toReal_mono _ gint
          simpa using int_f_ne_top
        _ = ENNReal.toReal (∫⁻ a : α, f a ∂μ) + δ := by
          rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
        _ < ENNReal.toReal (∫⁻ a : α, f a ∂μ) + ε := by gcongr
        _ = (∫⁻ a : α, ENNReal.ofReal ↑(f a) ∂μ).toReal + ε := by simp
-- 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
a : (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal = (∫⁻ (a : α), g a ∂μ).toReal
a₁ : (∫⁻ (a : α), g a ∂μ).toReal ≤ (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)).toReal
a₂ : (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)).toReal = (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
have a₃ : (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ) < (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑ε : ℝ)
Tactic: calc
        ENNReal.toReal (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) =
            ENNReal.toReal (∫⁻ a : α, g a ∂μ) := by congr 1
        _ ≤ ENNReal.toReal ((∫⁻ a : α, f a ∂μ) + δ) := by
          apply ENNReal.toReal_mono _ gint
          simpa using int_f_ne_top
        _ = ENNReal.toReal (∫⁻ a : α, f a ∂μ) + δ := by
          rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
        _ < ENNReal.toReal (∫⁻ a : α, f a ∂μ) + ε := by gcongr
        _ = (∫⁻ a : α, ENNReal.ofReal ↑(f a) ∂μ).toReal + ε := by simp
-- 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
a : (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal = (∫⁻ (a : α), g a ∂μ).toReal
a₁ : (∫⁻ (a : α), g a ∂μ).toReal ≤ (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)).toReal
a₂ : (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)).toReal = (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ)
a₃ : (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑δ : ℝ) < (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑ε : ℝ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
have a₄ : (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal + (↑ε : ℝ) = (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
Tactic: calc
        ENNReal.toReal (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) =
            ENNReal.toReal (∫⁻ a : α, g a ∂μ) := by congr 1
        _ ≤ ENNReal.toReal ((∫⁻ a : α, f a ∂μ) + δ) := by
          apply ENNReal.toReal_mono _ gint
          simpa using int_f_ne_top
        _ = ENNReal.toReal (∫⁻ a : α, f a ∂μ) + δ := by
          rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
        _ < ENNReal.toReal (∫⁻ a : α, f a ∂μ) + ε := by gcongr
        _ = (∫⁻ a : α, ENNReal.ofReal ↑(f a) ∂μ).toReal + ε := by simp
-- 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(f x) : ℝ)
have apply : ∀ (x : α), LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ (↑(f x) : ℝ)) x)
Tactic: apply Filter.Eventually.of_forall fun 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ)
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), (↑(f x) : ℝ≥0∞) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (↑δ : ℝ≥0∞)
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (g x).toReal
have apply : ∀ (x : α), LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ (g x).toReal) x)
Tactic: apply Filter.Eventually.of_forall fun 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
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have pos : ∀ (hc : c = 0),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: by_cases hc : c = 0
-- 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
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
pos :
  ∀ (hc : c = 0),
    ∃ (g : α → ℝ≥0),
      (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
        UpperSemicontinuous g ∧
          ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
            ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have neg : ∀ (hc : ¬c = 0),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: by_cases hc : c = 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
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have μs_lt_top : μ s < ∞ := by simpa [hs, hc, ENNReal.mul_eq_top, lt_top_iff_ne_top] using int_f
-- 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
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have this : 0 < ε / (↑c : ℝ≥0∞)
Tactic: have : (0 : ℝ≥0∞) < ε / c := ENNReal.div_pos_iff.2 ⟨ε0, ENNReal.coe_ne_top⟩
-- 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
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have neg : ∀ (F : Set α) (Fs : F ⊆ s) (F_closed : IsClosed F)
  (μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))),
  ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
Tactic: obtain ⟨F, Fs, F_closed, μF⟩ : ∃ (F : _), F ⊆ s ∧ IsClosed F ∧ μ s < μ F + ε / c :=
      hs.exists_isClosed_lt_add μs_lt_top.ne this.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
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : 0 < ε / (↑c : ℝ≥0∞)
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) (ε / (↑c : ℝ≥0∞))
⊢ ∃ (g : α → ℝ≥0),
    (∀ (x : α), g x ≤ (piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) ∧
      UpperSemicontinuous g ∧
        ∫⁻ (x : α), (↑((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ∂μ ≤
          ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + ε
have neg : ∀ (x : α),
  LE.le (α := ℝ≥0) (F.indicator (fun (x : α) ↦ c) x : ℝ≥0)
    ((piecewise s hs (const α c) (const α 0) : (a : α) → ℝ≥0) x : ℝ≥0)
Tactic: refine
      ⟨Set.indicator F fun _ => c, fun x => ?_, F_closed.upperSemicontinuous_indicator zero_le,
        ?_⟩