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 : α → ℝ
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
case : LowerSemicontinuous g
hf₁ : LowerSemicontinuous (β := EReal) fun (z : α) ↦ (↑(gp z) : EReal)
hg : LowerSemicontinuous (β := EReal) fun (z : α) ↦ -(↑(↑(gm z) : ℝ≥0∞) : EReal)
hcont :
  ∀ (x : α),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑(gp x) : EReal), -(↑(↑(gm x) : ℝ≥0∞) : EReal))
hg₁ : LowerSemicontinuous (β := EReal) fun (z : α) ↦ -(↑(↑(gm z) : ℝ≥0∞) : EReal)
hcont₁ hcont₂ :
  ∀ (x : α),
    ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 + p.2) ((↑(gp x) : EReal), -(↑(↑(gm x) : ℝ≥0∞) : EReal))
⊢ LowerSemicontinuous g

Tactic:
case lsc =>
    show LowerSemicontinuous g
    apply LowerSemicontinuous.add'
    · exact continuous_coe_ennreal_ereal.comp_lowerSemicontinuous gpcont fun x y hxy =>
          EReal.coe_ennreal_le_coe_ennreal_iff.2 hxy
    · apply continuous_neg.comp_upperSemicontinuous_antitone _ fun x y hxy =>
          EReal.neg_le_neg_iff.2 hxy
      dsimp
      apply continuous_coe_ennreal_ereal.comp_upperSemicontinuous _ fun x y hxy =>
          EReal.coe_ennreal_le_coe_ennreal_iff.2 hxy
      exact ENNReal.continuous_coe.comp_upperSemicontinuous gmcont fun x y hxy =>
          ENNReal.coe_le_coe.2 hxy
    · intro x
      exact EReal.continuousAt_add (by simp) (by simp)

Premises used: Iff.mpr, EReal.coe_ennreal_le_coe_ennreal_iff, ContinuousNeg.continuous_neg, EReal.neg_le_neg_iff, Continuous.comp_lowerSemicontinuous, ENNReal.coe_le_coe, Continuous.comp_upperSemicontinuous, continuous_coe_ennreal_ereal, LowerSemicontinuous, EReal.continuousAt_add, LowerSemicontinuous.add', ENNReal.continuous_coe, Continuous.comp_upperSemicontinuous_antitone
-- 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 < ε
rcases :
  ∀ (g : α → EReal) (g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x) (gcont : LowerSemicontinuous g)
    (g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ) (g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤)
    (gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε),
    ∃ (g : α → EReal),
      (∀ (x : α), g x < (↑(f x) : EReal)) ∧
        UpperSemicontinuous g ∧
          Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
            (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ ∫ (x : α), f x ∂μ < ∫ (x : α), (g x).toReal ∂μ + ε
⊢ ∃ (g : α → EReal),
    (∀ (x : α), g x < (↑(f x) : EReal)) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ ∫ (x : α), f x ∂μ < ∫ (x : α), (g x).toReal ∂μ + ε

Tactic:
rcases exists_lt_lowerSemicontinuous_integral_lt (fun x => -f x) hf.neg εpos with
    ⟨g, g_lt_f, gcont, g_integrable, g_lt_top, gint⟩

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.exists_lt_lowerSemicontinuous_integral_lt, Neg.neg
-- 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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
⊢ ∃ (g : α → EReal),
    (∀ (x : α), g x < (↑(f x) : EReal)) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ ∫ (x : α), f x ∂μ < ∫ (x : α), (g x).toReal ∂μ + ε

Tactic:
⟨fun x => -g x, ?_, ?_, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Neg.neg
-- 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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
refine_1 : ∀ (x : α), (fun (x : α) ↦ -g x) x < (↑(f x) : EReal)
refine_2 : UpperSemicontinuous (β := EReal) fun (x : α) ↦ -g x
refine_3 : Integrable (ε := ℝ) (fun (x : α) ↦ EReal.toReal ((fun (x : α) ↦ -g x) x)) μ
refine_4 : ∀ᵐ (x : α) ∂μ, LT.lt (α := EReal) ⊥ ((fun (x : α) ↦ -g x) x)
refine_5 : ∫ (x : α), f x ∂μ < ∫ (x : α), EReal.toReal ((fun (x : α) ↦ -g x) x) ∂μ + ε
⊢ ∃ (g : α → EReal),
    (∀ (x : α), g x < (↑(f x) : EReal)) ∧
      UpperSemicontinuous g ∧
        Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ ∧
          (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ ∫ (x : α), f x ∂μ < ∫ (x : α), (g x).toReal ∂μ + ε

Tactic:
refine ⟨fun x => -g 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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
x : α
⊢ -(↑(f x) : EReal) < g x

Tactic:
simpa only [EReal.coe_neg] using g_lt_f x

Premises used: EReal.coe_neg
-- 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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
⊢ ∀ (x : α), (fun (x : α) ↦ -g x) x < (↑(f x) : EReal)

Tactic:
exact fun x => EReal.neg_lt_comm.1 (by simpa only [EReal.coe_neg] using g_lt_f x)

Premises used: EReal.neg_lt_comm, Iff.mp
-- 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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
⊢ UpperSemicontinuous (β := EReal) fun (x : α) ↦ -g x

Tactic:
continuous_neg.comp_lowerSemicontinuous_antitone gcont fun x y hxy =>
        EReal.neg_le_neg_iff.2 hxy

Premises used: Iff.mpr, ContinuousNeg.continuous_neg, EReal.neg_le_neg_iff, Continuous.comp_lowerSemicontinuous_antitone
-- 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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
⊢ UpperSemicontinuous (β := EReal) fun (x : α) ↦ -g x

Tactic:
exact
      continuous_neg.comp_lowerSemicontinuous_antitone gcont fun x y hxy =>
        EReal.neg_le_neg_iff.2 hxy

Premises used: Iff.mpr, ContinuousNeg.continuous_neg, EReal.neg_le_neg_iff, Continuous.comp_lowerSemicontinuous_antitone
-- 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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
⊢ Integrable (ε := ℝ) (-fun (x : α) ↦ (g x).toReal) μ

Tactic:
g_integrable.neg

Premises used: MeasureTheory.Integrable.neg
-- 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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
h : ∀ (x : α), EReal.toReal ((fun (x : α) ↦ -g x) x) = (-fun (x : α) ↦ (g x).toReal) x
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ EReal.toReal ((fun (x : α) ↦ -g x) x)) μ

Tactic:
convert! g_integrable.neg

Premises used: MeasureTheory.Integrable.neg
-- 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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
x : α
⊢ EReal.toReal ((fun (x : α) ↦ -g x) x) = (-fun (x : α) ↦ (g x).toReal) 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
inst_4 : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := EReal) ⊥ ((fun (x : α) ↦ -g x) x)

Tactic:
simpa [bot_lt_iff_ne_bot, lt_top_iff_ne_top] using g_lt_top

Premises used: bot_lt_iff_ne_bot, lt_top_iff_ne_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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (x : α), (g x).toReal ∂μ) < ε

Tactic:
simp_rw [integral_neg, lt_neg_add_iff_add_lt] at gint

Premises used: MeasureTheory.integral_neg, lt_neg_add_iff_add_lt
-- 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 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : HAdd.hAdd (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (x : α), (g x).toReal ∂μ) < ε
⊢ HAdd.hAdd (α := ℝ) (∫ (x : α), (g x).toReal ∂μ) (∫ (a : α), f a ∂μ) < ε

Tactic:
rw [add_comm] at gint

Premises used: add_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 : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), (↑(-f x) : EReal) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (ε := ℝ) (fun (x : α) ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : HAdd.hAdd (α := ℝ) (∫ (x : α), (g x).toReal ∂μ) (∫ (a : α), f a ∂μ) < ε
⊢ ∫ (x : α), f x ∂μ < ∫ (x : α), EReal.toReal ((fun (x : α) ↦ -g x) x) ∂μ + ε

Tactic:
simpa [integral_neg] using gint

Premises used: MeasureTheory.integral_neg
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ nndist (α := ℝ≥0) (((0 : X →ᵇ ℝ≥0) : (a : X) → ℝ≥0) x : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) ≤ nndist 0 f

Tactic:
nndist_coe_le_nndist x

Premises used: BoundedContinuousFunction.nndist_coe_le_nndist
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
h : (f : (a : X) → ℝ≥0) x = nndist (α := ℝ≥0) (((0 : X →ᵇ ℝ≥0) : (a : X) → ℝ≥0) x : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ (f : (a : X) → ℝ≥0) x ≤ nndist 0 f

Tactic:
convert! nndist_coe_le_nndist x

Premises used: BoundedContinuousFunction.nndist_coe_le_nndist
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ (f : (a : X) → ℝ≥0) x = nndist (α := ℝ≥0) (((0 : X →ᵇ ℝ≥0) : (a : X) → ℝ≥0) x : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
simp only [coe_zero, Pi.zero_apply, NNReal.nndist_zero_eq_val]

Premises used: Pi.zero_apply, BoundedContinuousFunction.coe_zero, NNReal.nndist_zero_eq_val
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ ∫⁻ (a : X), (↑(nndist 0 f) : ℝ≥0∞) ∂μ ≤ HMul.hMul (β := ℝ≥0∞) (edist 0 f) ((μ : (a : Set X) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ Measurable (β := ℝ≥0∞) fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞)

Tactic:
measurable_coe_nnreal_ennreal.comp f.continuous.measurable

Premises used: ENNReal.ofNNReal, Measurable.comp, BoundedContinuousFunction.continuous, WithTop.some, Continuous.measurable, measurable_coe_nnreal_ennreal
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
f_bdd : ∃ (c : ℝ≥0), ∀ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞)
⊢ ∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ < ∞

Tactic:
apply IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal

Premises used: IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
⊢ ∃ (c : ℝ≥0), ∀ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞)

Tactic:
⟨nndist f 0, fun x ↦ ?_⟩

Premises used: NNDist.nndist, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
f_bdd : ∀ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(nndist f 0) : ℝ≥0∞)
⊢ ∃ (c : ℝ≥0), ∀ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞)

Tactic:
refine ⟨nndist f 0, fun x ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
x : X
⊢ (f : (a : X) → ℝ≥0) x ≤ nndist f 0

Tactic:
have key := BoundedContinuousFunction.NNReal.upper_bound f x
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
x : X
key f_bdd f_bdd₁ f_bdd₂ f_bdd₃ : (f : (a : X) → ℝ≥0) x ≤ nndist f 0
⊢ (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ≤ (↑(nndist f 0) : ℝ≥0∞)

Tactic:
rwa [ENNReal.coe_le_coe]

Premises used: ENNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
inst_3 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ Integrable (NNReal.toReal ∘ (⇑f : (a : X) → ℝ≥0)) μ

Tactic:
⟨(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable, ?_⟩

Premises used: Measurable.aestronglyMeasurable, Continuous.comp, NNReal.continuous_coe, MeasureTheory.Integrable, BoundedContinuousFunction.continuous, And.intro, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
inst_3 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
refine : HasFiniteIntegral (NNReal.toReal ∘ (⇑f : (a : X) → ℝ≥0)) μ
⊢ Integrable (NNReal.toReal ∘ (⇑f : (a : X) → ℝ≥0)) μ

Tactic:
refine ⟨(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
inst_3 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
simp : ∫⁻ (a : X), (↑((f : (a : X) → ℝ≥0) a) : ℝ≥0∞) ∂μ < ∞
⊢ HasFiniteIntegral (NNReal.toReal ∘ (⇑f : (a : X) → ℝ≥0)) μ

Tactic:
simp only [hasFiniteIntegral_iff_enorm, Function.comp_apply, NNReal.enorm_eq]

Premises used: NNReal.enorm_eq, Function.comp_apply, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
inst_3 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ ∫⁻ (a : X), (↑((f : (a : X) → ℝ≥0) a) : ℝ≥0∞) ∂μ < ∞

Tactic:
lintegral_lt_top_of_nnreal _ f

Premises used: BoundedContinuousFunction.lintegral_lt_top_of_nnreal
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
inst_3 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ ∫⁻ (a : X), (↑((f : (a : X) → ℝ≥0) a) : ℝ≥0∞) ∂μ < ∞

Tactic:
exact lintegral_lt_top_of_nnreal _ f

Premises used: BoundedContinuousFunction.lintegral_lt_top_of_nnreal
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
inst_3 : OpensMeasurableSpace X
f : X →ᵇ ℝ
simp :
  HSub.hSub (α := ℝ) (∫ (a : X), (NNReal.toReal ∘ (⇑f.nnrealPart : (a : X) → ℝ≥0)) a ∂μ)
      (∫ (a : X), (NNReal.toReal ∘ (⇑(-f).nnrealPart : (a : X) → ℝ≥0)) a ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : X), (↑((f.nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂μ)
      (∫ (x : X), (↑(((-f).nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂μ)
⊢ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : X), (↑((f.nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂μ)
      (∫ (x : X), (↑(((-f).nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂μ)

Tactic:
simp only [f.self_eq_nnrealPart_sub_nnrealPart_neg, Pi.sub_apply, integral_sub,
             integrable_of_nnreal]

Premises used: MeasureTheory.integral_sub, BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg, Pi.sub_apply, BoundedContinuousFunction.integrable_of_nnreal
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
inst_3 : OpensMeasurableSpace X
f : X →ᵇ ℝ
⊢ HSub.hSub (α := ℝ) (∫ (a : X), (NNReal.toReal ∘ (⇑f.nnrealPart : (a : X) → ℝ≥0)) a ∂μ)
      (∫ (a : X), (NNReal.toReal ∘ (⇑(-f).nnrealPart : (a : X) → ℝ≥0)) a ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : X), (↑((f.nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂μ)
      (∫ (x : X), (↑(((-f).nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂μ)

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
f : X →ᵇ ℝ
⊢ ∫⁻ (x : X), ENNReal.ofReal ((f : (a : X) → ℝ) x) ∂μ < ∞

Tactic:
lintegral_lt_top_of_nnreal _ f.nnrealPart

Premises used: ENNReal.ofReal, BoundedContinuousFunction.lintegral_lt_top_of_nnreal, NNReal.mk, BoundedContinuousFunction.nnrealPart, Real.toNNReal
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)) μ

Tactic:
simpa [Function.comp_apply] using
        (NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, Continuous.comp, NNReal.continuous_coe, BoundedContinuousFunction.continuous, Continuous.measurable, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
rw :
  (∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ).toReal =
    (∫⁻ (a : X), ENNReal.ofReal (↑((f : (a : X) → ℝ≥0) a) : ℝ) ∂μ).toReal
rw₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)
⊢ (∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ).toReal = ∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂μ

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae _ (by simpa [Function.comp_apply] using
        (NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable)]

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ).toReal =
    (∫⁻ (a : X), ENNReal.ofReal (↑((f : (a : X) → ℝ≥0) a) : ℝ) ∂μ).toReal

Tactic:
simp only [ENNReal.ofReal_coe_nnreal]

Premises used: ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ ∀ (x : X), LE.le (α := ℝ) (0 x) ((fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)) x)

Tactic:
simp