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
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 (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ) = (∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)).toReal
have h : (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ) =
  (∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ).toReal + (↑ε : ℝ≥0∞).toReal
Tactic: rw [ENNReal.toReal_add Ig.ne 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
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∞) ∂μ < ∞
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(g x) : ℝ)
have refine_2 : ∀ (x : α), LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ (↑(g x) : ℝ)) x)
Tactic: apply Filter.Eventually.of_forall
-- 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∞) ∂μ < ∞
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(f x) : ℝ)
have refine_2 : ∀ (x : α), LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ (↑(f x) : ℝ)) x)
Tactic: apply Filter.Eventually.of_forall
-- 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
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
have δpos : 0 < δ
Tactic: have δpos : 0 < δ := half_pos ε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
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
have int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
Tactic: have int_fp : Integrable (fun x => (fp x : ℝ)) μ := hf.real_toNNReal
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
have rcases : ∀ (gp : α → ℝ≥0∞) (fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x) (gpcont : LowerSemicontinuous gp)
  (gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞) (gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ)
  (gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)),
  ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
Tactic: rcases exists_lt_lowerSemicontinuous_integral_gt_nnreal fp int_fp δpos with
    ⟨gp, fp_lt_gp, gpcont, gp_lt_top, gp_integrable, gpint⟩
-- 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
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
have int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
Tactic: have int_fm : Integrable (fun x => (fm x : ℝ)) μ := hf.neg.real_toNNReal
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
have rcases : ∀ (gm : α → ℝ≥0) (gm_le_fm : ∀ (x : α), gm x ≤ fm x) (gmcont : UpperSemicontinuous gm)
  (gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ)
  (gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ),
  ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
Tactic: rcases exists_upperSemicontinuous_le_integral_le fm int_fm δpos with
    ⟨gm, gm_le_fm, gmcont, gm_integrable, gmint⟩
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ
gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
⊢ ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
have h : ∀ (a : α) (hx : gp a < ∞), (g a).toReal = (↑(gp a) : EReal).toReal - (↑(↑(gm a) : ℝ≥0∞) : EReal).toReal
Tactic: filter_upwards [gp_lt_top] with _ hx
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ
gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
a : α
hx : gp a < ∞
⊢ (g a).toReal = (↑(gp a) : EReal).toReal - (↑(↑(gm a) : ℝ≥0∞) : EReal).toReal
have h : (↑(gp a) : EReal) ≠ ⊤
Tactic: rw [EReal.toReal_sub]
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ
gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
a : α
hx : gp a < ∞
h : (↑(gp a) : EReal) ≠ ⊤
⊢ (g a).toReal = (↑(gp a) : EReal).toReal - (↑(↑(gm a) : ℝ≥0∞) : EReal).toReal
have h₁ : (↑(gp a) : EReal) ≠ ⊥
Tactic: rw [EReal.toReal_sub]
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ
gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
a : α
hx : gp a < ∞
h : (↑(gp a) : EReal) ≠ ⊤
h₁ : (↑(gp a) : EReal) ≠ ⊥
⊢ (g a).toReal = (↑(gp a) : EReal).toReal - (↑(↑(gm a) : ℝ≥0∞) : EReal).toReal
have h₂ : (↑(↑(gm a) : ℝ≥0∞) : EReal) ≠ ⊤
Tactic: rw [EReal.toReal_sub]
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ
gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
a : α
hx : gp a < ∞
h : (↑(gp a) : EReal) ≠ ⊤
h₁ : (↑(gp a) : EReal) ≠ ⊥
h₂ : (↑(↑(gm a) : ℝ≥0∞) : EReal) ≠ ⊤
⊢ (g a).toReal = (↑(gp a) : EReal).toReal - (↑(↑(gm a) : ℝ≥0∞) : EReal).toReal
have h₃ : (↑(↑(gm a) : ℝ≥0∞) : EReal) ≠ ⊥
Tactic: rw [EReal.toReal_sub]
-- 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
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ
gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
have ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
Tactic: have ae_g : ∀ᵐ x ∂μ, (g x).toReal = (gp x : EReal).toReal - (gm x : EReal).toReal := by
    filter_upwards [gp_lt_top] with _ hx
    rw [EReal.toReal_sub] <;> simp [hx.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
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ
gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
have refine : ∀ (x : α), (↑(f x) : EReal) < g x
Tactic: refine ⟨g, ?lt, ?lsc, ?int, ?aelt, ?intlt⟩
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ
gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
refine : ∀ (x : α), (↑(f x) : EReal) < g x
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
have refine₁ : LowerSemicontinuous g
Tactic: refine ⟨g, ?lt, ?lsc, ?int, ?aelt, ?intlt⟩
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ
gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
refine : ∀ (x : α), (↑(f x) : EReal) < g x
refine₁ : LowerSemicontinuous g
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
have refine₂ : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
Tactic: refine ⟨g, ?lt, ?lsc, ?int, ?aelt, ?intlt⟩
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
int_fp : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), (↑(fp x) : ℝ≥0∞) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), (↑(fp x) : ℝ) ∂μ + (↑δ : ℝ)
fm : α → ℝ≥0 := fun (x : α) ↦ (-f x).toNNReal
int_fm : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(gm x) : ℝ)) μ
gmint : ∫ (x : α), (↑(fm x) : ℝ) ∂μ - (↑δ : ℝ) ≤ ∫ (x : α), (↑(gm x) : ℝ) ∂μ
g : α → EReal := fun (x : α) ↦ (↑(gp x) : EReal) - (↑(↑(gm x) : ℝ≥0∞) : EReal)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal
refine : ∀ (x : α), (↑(f x) : EReal) < g x
refine₁ : LowerSemicontinuous g
refine₂ : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
⊢ ∃ (g : α → EReal),
    (∀ (x : α), (↑(f x) : EReal) < g x) ∧
      LowerSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
have refine₃ : ∀ᵐ (x : α) ∂μ, g x < ⊤
Tactic: refine ⟨g, ?lt, ?lsc, ?int, ?aelt, ?intlt⟩