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
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 : α) ∂μ, ‖(↑(g a) : ℝ)‖ ≤ ‖(↑(f a) : ℝ)‖

Tactic:
exact Filter.Eventually.of_forall fun x => by simp [gf x]

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
refine_2 :
  (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal - (↑ε : ℝ) ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal
refine_2₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(g x) : ℝ)
refine_2₂ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ
refine_2₃ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(f x) : ℝ)
refine_2₄ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
⊢ ∫ (x : α), (↑(f x) : ℝ) ∂μ - (↑ε : ℝ) ≤ ∫ (x : α), (↑(g x) : ℝ) ∂μ

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
refine_2 :
  (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal - (↑ε : ℝ) ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal

Tactic:
rw [sub_le_iff_le_add]

Premises used: sub_le_iff_le_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
⊢ (∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ).toReal ≤ (∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)).toReal

Tactic:
ENNReal.toReal_mono _ gint

Premises used: ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
h : ∀ (x : α), ENNReal.ofReal (↑(f x) : ℝ) = (↑(f x) : ℝ≥0∞)
h₁ :
  (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ) = (∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)).toReal
refine_2 : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞) ≠ ∞
⊢ (∫⁻ (a : α), ENNReal.ofReal (↑(f a) : ℝ) ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ)

Tactic:
convert! ENNReal.toReal_mono _ gint

Premises used: ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
x : α
⊢ ENNReal.ofReal (↑(f x) : ℝ) = (↑(f x) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
h :
  (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ) =
    (∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ).toReal + (↑ε : ℝ≥0∞).toReal
⊢ (∫⁻ (a : α), ENNReal.ofReal (↑(g a) : ℝ) ∂μ).toReal + (↑ε : ℝ) = (∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)).toReal

Tactic:
rw [ENNReal.toReal_add Ig.ne ENNReal.coe_ne_top]

Premises used: ENNReal.toReal_add, LT.lt.ne, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞) ∂μ).toReal + (↑ε : ℝ≥0∞).toReal

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
⊢ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞) ≠ ∞

Tactic:
simpa using Ig.ne

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
refine_2 : ∀ (x : α), LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ (↑(g x) : ℝ)) x)
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(g x) : ℝ)

Tactic:
apply Filter.Eventually.of_forall

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
⊢ ∀ (x : α), LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ (↑(g x) : ℝ)) x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞) ∂μ < ∞
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ

Tactic:
gcont.measurable.coe_nnreal_real.aemeasurable.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, Measurable.aemeasurable, UpperSemicontinuous.measurable, Measurable.coe_nnreal_real
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞) ∂μ < ∞
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(g x) : ℝ)) μ

Tactic:
exact gcont.measurable.coe_nnreal_real.aemeasurable.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, Measurable.aemeasurable, UpperSemicontinuous.measurable, Measurable.coe_nnreal_real
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
refine_2 : ∀ (x : α), LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ (↑(f x) : ℝ)) x)
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (↑(f x) : ℝ)

Tactic:
apply Filter.Eventually.of_forall

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
ε : ℝ≥0
εpos : 0 < (↑ε : ℝ≥0∞)
If : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), (↑(f x) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ + (↑ε : ℝ≥0∞)
Ig : ∫⁻ (x : α), (↑(g x) : ℝ≥0∞) ∂μ < ∞
⊢ ∀ (x : α), LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ (↑(f x) : ℝ)) x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞) ∂μ < ∞
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ

Tactic:
fint.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
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∞) ∂μ < ∞
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ

Tactic:
exact fint.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
⊢ 0 < δ

Tactic:
have δpos : 0 < δ := half_pos εpos
-- 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun (x : α) ↦ (f x).toNNReal
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fp x) : ℝ)) μ

Tactic:
have int_fp : Integrable (fun x => (fp x : ℝ)) μ := hf.real_toNNReal
-- 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 : α → ℝ
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) : ℝ)) μ
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 ∂μ + ε
⊢ ∃ (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⟩

Premises used: MeasureTheory.exists_lt_lowerSemicontinuous_integral_gt_nnreal
-- 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 : α → ℝ
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
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (↑(fm x) : ℝ)) μ

Tactic:
have int_fm : Integrable (fun x => (fm x : ℝ)) μ := hf.neg.real_toNNReal
-- 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 : α → ℝ
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) : ℝ)) μ
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 ∂μ + ε
⊢ ∃ (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⟩

Premises used: MeasureTheory.exists_upperSemicontinuous_le_integral_le
-- 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 : α → ℝ
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)
h : ∀ (a : α) (hx : gp a < ∞), (g a).toReal = (↑(gp a) : EReal).toReal - (↑(↑(gm a) : ℝ≥0∞) : EReal).toReal
⊢ ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x) : EReal).toReal - (↑(↑(gm x) : ℝ≥0∞) : EReal).toReal

Tactic:
filter_upwards [gp_lt_top] with _ hx
-- 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 : α → ℝ
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) ≠ ⊤
h₃ : (↑(↑(gm a) : ℝ≥0∞) : EReal) ≠ ⊥
⊢ (g a).toReal = (↑(gp a) : EReal).toReal - (↑(↑(gm a) : ℝ≥0∞) : EReal).toReal

Tactic:
rw [EReal.toReal_sub]

Premises used: EReal.toReal_sub
-- 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 : α → ℝ
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 < ∞
⊢ (↑(gp a) : EReal) ≠ ⊤

Tactic:
simp [hx.ne]

Premises used: LT.lt.ne
-- 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 : α → ℝ
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 < ∞
⊢ (↑(gp a) : EReal) ≠ ⊥

Tactic:
simp [hx.ne]

Premises used: LT.lt.ne
-- 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 : α → ℝ
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 < ∞
⊢ (↑(↑(gm a) : ℝ≥0∞) : EReal) ≠ ⊤

Tactic:
simp [hx.ne]

Premises used: LT.lt.ne