awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
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∞) ∂μ + ε
⊢ ∃ (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⟩

Premises used: MeasureTheory.exists_lt_lowerSemicontinuous_lintegral_ge, AEMeasurable.mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
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∞) ∂μ + ε
⊢ ∃ (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⟩

Premises used: AEMeasurable.ae_eq_mk, MeasureTheory.exists_measurable_superset_of_null
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞)
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∞) ∂μ + ε
⊢ ∃ (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⟩

Premises used: MeasureTheory.exists_le_lowerSemicontinuous_lintegral_ge, Set.indicator, Measurable.indicator, measurable_const, Top.top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞) ∂μ + ε

Tactic:
⟨fun x => g0 x + g1 x, fun x => ?_, g0_cont.add g1_cont, ?_⟩

Premises used: LowerSemicontinuous.add, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
refine_2 : ∫⁻ (x : α), (fun (x : α) ↦ g0 x + g1 x) x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε
⊢ ∃ (g : α → ℝ≥0∞),
    (∀ (x : α), (↑(f x) : ℝ≥0∞) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε

Tactic:
refine ⟨fun x => g0 x + g1 x, fun x => ?_, g0_cont.add g1_cont, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
neg : ∀ (h : x ∉ s), (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
⊢ (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x

Tactic:
by_cases h : x ∈ s
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
⊢ s.indicator (fun (_x : α) ↦ ∞) x ≤ g1 x

Tactic:
have := le_g1 x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
⊢ g1 x = ∞

Tactic:
simp only [h, Set.indicator_of_mem, top_le_iff] at this

Premises used: Set.indicator_of_mem, top_le_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 : g1 x = ∞
⊢ (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x

Tactic:
simp [this]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
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
⊢ f x = AEMeasurable.mk f fmeas x

Tactic:
rw [Set.compl_subset_comm] at hs

Premises used: Set.compl_subset_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 : 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:
hs h

Premises used: Set.Mem, setOf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 : 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:
exact hs h
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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

Tactic:
have : f x = fmeas.mk f x := by rw [Set.compl_subset_comm] at hs; exact hs h
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
neg : (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x
⊢ (↑(f x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
⊢ (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x

Tactic:
(f_lt_g0 x).trans_le le_self_add

Premises used: LT.lt.trans_le, le_self_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
⊢ (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) < (fun (x : α) ↦ g0 x + g1 x) x

Tactic:
exact (f_lt_g0 x).trans_le le_self_add

Premises used: LT.lt.trans_le, le_self_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 + g1 x ∂μ = ∫⁻ (x : α), g0 x ∂μ + ∫⁻ (x : α), g1 x ∂μ

Tactic:
lintegral_add_left g0_cont.measurable _

Premises used: MeasureTheory.lintegral_add_left, LowerSemicontinuous.measurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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)

Tactic:
add_le_add ?_ ?_

Premises used: add_le_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2
refine_2 : ∫⁻ (x : α), g1 x ∂μ ≤ 0 + ε / 2
⊢ ∫⁻ (x : α), g0 x ∂μ + ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2 + (0 + ε / 2)

Tactic:
refine add_le_add ?_ ?_

Premises used: add_le_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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 : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ + ε / 2

Tactic:
g0_int
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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
h : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ = ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ
⊢ ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ + ε / 2

Tactic:
convert! g0_int using 2
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞) ∂μ = ∫⁻ (x : α), (↑(AEMeasurable.mk f fmeas x) : ℝ≥0∞) ∂μ

Tactic:
lintegral_congr_ae (fmeas.ae_eq_mk.fun_comp _)

Premises used: MeasureTheory.lintegral_congr_ae, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.fun_comp