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
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
x : α
⊢ (↑(f x) : ℝ≥0∞) < g x
have x₁ : (↑(f x) : ℝ≥0∞) < f' x
Tactic: calc
      (f x : ℝ≥0∞) < f' x := by
        simpa only [← ENNReal.coe_lt_coe, add_zero] using add_lt_add_right (wpos x) (f x)
      _ ≤ g x := le_g 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
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) + (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 =
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2
have rw : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ + ∫⁻ (a : α), (↑(w a) : ℝ≥0∞) ∂μ + ε / 2 =
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2
Tactic: rw [lintegral_add_right _ wmeas.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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 ≤
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2
have grw : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2 ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2
Tactic: grw [wint]
-- 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
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2 = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have rw : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2) = ∫⁻ (x : α), (↑(f 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
rw : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + (ε / 2 + ε / 2) = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
⊢ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2 = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have rw₁ : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε = ∫⁻ (x : α), (↑(f 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have x : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) + (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 =
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2
Tactic: calc
      (∫⁻ x : α, g x ∂μ) ≤ (∫⁻ x : α, f x + w x ∂μ) + ε / 2 := gint
      _ = ((∫⁻ x : α, f x ∂μ) + ∫⁻ x : α, w x ∂μ) + ε / 2 := by
        rw [lintegral_add_right _ wmeas.coe_nnreal_ennreal]
      _ ≤ (∫⁻ x : α, f x ∂μ) + ε / 2 + ε / 2 := by grw [wint]
      _ = (∫⁻ x : α, f 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
x :
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) + (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 =
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have x₁ : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2
Tactic: calc
      (∫⁻ x : α, g x ∂μ) ≤ (∫⁻ x : α, f x + w x ∂μ) + ε / 2 := gint
      _ = ((∫⁻ x : α, f x ∂μ) + ∫⁻ x : α, w x ∂μ) + ε / 2 := by
        rw [lintegral_add_right _ wmeas.coe_nnreal_ennreal]
      _ ≤ (∫⁻ x : α, f x ∂μ) + ε / 2 + ε / 2 := by grw [wint]
      _ = (∫⁻ x : α, f 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : Measurable f
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
w : α → ℝ≥0
wpos : ∀ (x : α), 0 < w x
wmeas : Measurable w
wint : ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ < ε / 2
f' : (x : α) → ℝ≥0∞ := fun (x : α) ↦ (↑(f x + w x) : ℝ≥0∞)
g : α → ℝ≥0∞
le_g : ∀ (x : α), f' x ≤ g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2
x :
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) + (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 =
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2
x₁ :
  ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ∫⁻ (x : α), (↑(w x) : ℝ≥0∞) ∂μ + ε / 2 ≤
    ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have x₂ : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + ε / 2 = ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
Tactic: calc
      (∫⁻ x : α, g x ∂μ) ≤ (∫⁻ x : α, f x + w x ∂μ) + ε / 2 := gint
      _ = ((∫⁻ x : α, f x ∂μ) + ∫⁻ x : α, w x ∂μ) + ε / 2 := by
        rw [lintegral_add_right _ wmeas.coe_nnreal_ennreal]
      _ ≤ (∫⁻ x : α, f x ∂μ) + ε / 2 + ε / 2 := by grw [wint]
      _ = (∫⁻ x : α, f x ∂μ) + ε := by rw [add_assoc, 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have this : ε / 2 ≠ 0
Tactic: have : ε / 2 ≠ 0 := (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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have rcases : ∀ (g0 : α → ℝ≥0∞) (f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x) (g0_cont : LowerSemicontinuous g0)
  (g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2),
  ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
Tactic: rcases exists_lt_lowerSemicontinuous_lintegral_ge μ (fmeas.mk f) fmeas.measurable_mk this with
    ⟨g0, f_lt_g0, g0_cont, g0_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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have rcases : ∀ (s : Set α) (hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s) (smeas : MeasurableSet s)
  (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
Tactic: rcases exists_measurable_superset_of_null fmeas.ae_eq_mk with ⟨s, hs, smeas, μs⟩
-- 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
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have rcases : ∀ (g1 : α → ℝ≥0∞) (le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x) (g1_cont : LowerSemicontinuous g1)
  (g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2),
  ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
Tactic: rcases exists_le_lowerSemicontinuous_lintegral_ge μ (s.indicator fun _x => ∞)
      (measurable_const.indicator smeas) this with
    ⟨g1, le_g1, g1_cont, g1_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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have refine_1 : ∀ (x : α), (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
Tactic: refine ⟨fun x => g0 x + g1 x, fun x => ?_, g0_cont.add g1_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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
refine_1 : ∀ (x : α), (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
have refine_2 : ∫⁻ (x : α), (fun (x : α) ↦ g0 x + g1 x) x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
Tactic: refine ⟨fun x => g0 x + g1 x, fun x => ?_, g0_cont.add g1_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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
x : α
⊢ (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
have pos : ∀ (h : x ∈ s), (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
Tactic: by_cases h : x ∈ s
-- 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
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
x : α
pos : ∀ (h : x ∈ s), (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
⊢ (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
have neg : ∀ (h : x ∉ s), (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
Tactic: by_cases h : x ∈ s
-- 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 : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∈ s
⊢ (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
have this₁ : s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
Tactic: have := le_g1 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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this_1 : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∈ s
this : s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
⊢ (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
have this₁ : g1 x = ∞
Tactic: simp only [h, Set.indicator_of_mem, top_le_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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∉ s
⊢ f x = AEMeasurable.mk f fmeas x
have rw : ∀ (hs : sᶜ ⊆ {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}) (smeas : MeasurableSet s)
  (μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)) (g1 : α → ℝ≥0∞)
  (le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x) (g1_cont : LowerSemicontinuous g1)
  (g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2) (x : α) (h : x ∉ s),
  f x = AEMeasurable.mk f fmeas x
Tactic: rw [Set.compl_subset_comm] at hs
Cleared hypotheses: hs, smeas, μs, g1, le_g1, g1_cont, g1_int, x, h
-- 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 : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∉ s
⊢ (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
have this₁ : f x = AEMeasurable.mk f fmeas x
Tactic: have : f x = fmeas.mk f x := by rw [Set.compl_subset_comm] at hs; exact hs h
-- 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
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this_1 : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∉ s
this : f x = AEMeasurable.mk f fmeas x
⊢ (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
have neg : (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
Tactic: rw [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
inst_4 : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2
s : Set α
hs : {x : α | (fun (x : α) ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun (_x : α) ↦ ∞) x ∂μ + ε / 2
⊢ ∫⁻ (x : α), g0 x ∂μ + ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + (0 + ε / 2)
have refine_1 : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2
Tactic: refine add_le_add ?_ ?_