awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ)
    (∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ.trim hm)

Tactic:
integral_trim hm hf.stronglyMeasurable_mk

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.integral_trim
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ)
    (∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ.trim hm)

Tactic:
exact integral_trim hm hf.stronglyMeasurable_mk

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.integral_trim
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
pos :
  ∀ (hr : r = 0),
    eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
neg :
  ∀ (hr : ¬r = 0),
    eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
this : f =ᶠ[ae μ] 0
rw :
  eLpNorm (ε := ℝ) 0 1 μ ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
rw₁ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
rw₂ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑0 : ℝ≥0∞)
rw₃ : 0 ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * 0
rw₄ rw₅ : LE.le (α := ℝ≥0∞) 0 0
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)

Tactic:
rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]

Premises used: MeasureTheory.eLpNorm_zero, MulZeroClass.mul_zero, ENNReal.coe_zero, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
pos : f =ᶠ[ae μ] 0
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)

Tactic:
suffices f =ᵐ[μ] 0 by
      rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑0 : ℝ)

Tactic:
rw [hr] at hf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : r = 0
hf₁ : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑0 : ℝ)
⊢ r = 0

Tactic:
rw [hr] at hf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑0 : ℝ)
hr : r = 0
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ 0

Tactic:
norm_cast at hf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
rw : Eq (α := ℝ) (∫ (a : α), f a ∂μ) 0
⊢ Eq (α := ℝ) (∫ (x : α), -f x ∂μ) 0

Tactic:
rw [integral_neg, neg_eq_zero]

Premises used: MeasureTheory.integral_neg, neg_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ Eq (α := ℝ) (∫ (a : α), f a ∂μ) 0

Tactic:
le_antisymm (integral_nonpos_of_ae hf) hfint'

Premises used: MeasureTheory.integral_nonpos_of_ae, le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ Eq (α := ℝ) (∫ (a : α), f a ∂μ) 0

Tactic:
exact le_antisymm (integral_nonpos_of_ae hf) hfint'

Premises used: MeasureTheory.integral_nonpos_of_ae, le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ Eq (α := ℝ) (∫ (x : α), -f x ∂μ) 0

Tactic:
have hnegf : ∫ x, -f x ∂μ = 0 := by
      rw [integral_neg, neg_eq_zero]
      exact le_antisymm (integral_nonpos_of_ae hf) hfint'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : Eq (α := ℝ) (∫ (x : α), -f x ∂μ) 0
pos : ∀ (this : -f =ᶠ[ae μ] 0), f =ᶠ[ae μ] 0
pos₁ : 0 ≤ᶠ[ae μ] -f
⊢ f =ᶠ[ae μ] 0

Tactic:
have := (integral_eq_zero_iff_of_nonneg_ae ?_ hfint.neg).1 hnegf
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : Eq (α := ℝ) (∫ (x : α), -f x ∂μ) 0
this : -f =ᶠ[ae μ] 0
h : ∀ (ω : α) (hω : (-f) ω = 0 ω), f ω = 0 ω
⊢ f =ᶠ[ae μ] 0

Tactic:
filter_upwards [this] with ω hω
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : Eq (α := ℝ) (∫ (x : α), -f x ∂μ) 0
this : -f =ᶠ[ae μ] 0
ω : α
hω : (-f) ω = 0 ω
h : ∀ (hω : -f ω = 0 ω), f ω = 0 ω
h₁ : ∀ (hω : -f ω = 0), f ω = 0 ω
h₂ h₃ h₄ h₅ : ∀ (hω : f ω = 0), f ω = 0 ω
⊢ f ω = 0 ω

Tactic:
rwa [Pi.neg_apply, Pi.zero_apply, neg_eq_zero] at hω

Premises used: Pi.zero_apply, neg_eq_zero, Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : Eq (α := ℝ) (∫ (x : α), -f x ∂μ) 0
h : ∀ (ω : α) (hω : f ω ≤ 0), 0 ω ≤ (-f) ω
⊢ 0 ≤ᶠ[ae μ] -f

Tactic:
filter_upwards [hf] with ω hω
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : Eq (α := ℝ) (∫ (x : α), -f x ∂μ) 0
ω : α
hω : f ω ≤ 0
h : 0 ≤ (-f) ω
h₁ : 0 ≤ -f ω
h₂ h₃ h₄ h₅ : f ω ≤ 0
⊢ 0 ω ≤ (-f) ω

Tactic:
rwa [Pi.zero_apply, Pi.neg_apply, Right.nonneg_neg_iff]

Premises used: Right.nonneg_neg_iff, Pi.zero_apply, Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
pos :
  ∀ (hμ : IsFiniteMeasure μ),
    eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
neg :
  ∀ (hμ : ¬IsFiniteMeasure μ),
    eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)

Tactic:
by_cases hμ : IsFiniteMeasure μ

Premises used: MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
by_contra : ∀ (hμ' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)), False
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
by_contra hμ'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
hμ' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ False

Tactic:
hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')

Premises used: Iff.mpr, lt_top_iff_ne_top, MeasureTheory.IsFiniteMeasure.mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
hμ' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ False

Tactic:
exact hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')

Premises used: Iff.mpr, lt_top_iff_ne_top, MeasureTheory.IsFiniteMeasure.mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have : μ Set.univ = ∞ := by
      by_contra hμ'
      exact hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
neg : eLpNorm f 1 μ ≤ ∞
neg₁ : ¬(↑r : ℝ≥0∞) = 0
neg₂ : ¬Eq (α := ℝ≥0∞) 2 0
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)

Tactic:
rw [this, ENNReal.mul_top', if_neg, ENNReal.top_mul', if_neg]

Premises used: ENNReal.mul_top', ENNReal.top_mul', if_neg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ eLpNorm f 1 μ ≤ ∞

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ eLpNorm f 1 μ ≤ ∞

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ¬(↑r : ℝ≥0∞) = 0

Tactic:
simp [hr]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ¬Eq (α := ℝ≥0∞) 2 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ : IsFiniteMeasure μ
⊢ IsFiniteMeasure μ

Tactic:
haveI := hμ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)

Tactic:
rw [integral_eq_integral_pos_part_sub_integral_neg_part hfint, sub_nonneg] at hfint'

Premises used: MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hfint'₁ : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)

Tactic:
rw [integral_eq_integral_pos_part_sub_integral_neg_part hfint, sub_nonneg] at hfint'

Premises used: MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hfint'₁ : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf₁ : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
⊢ ¬r = 0

Tactic:
rw [integral_eq_integral_pos_part_sub_integral_neg_part hfint, sub_nonneg] at hfint'

Premises used: MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hfint'₁ : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf₁ : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr₁ : ¬r = 0
⊢ IsFiniteMeasure μ

Tactic:
rw [integral_eq_integral_pos_part_sub_integral_neg_part hfint, sub_nonneg] at hfint'

Premises used: MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hfint'₁ : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf₁ : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr₁ : ¬r = 0
hμ₁ : IsFiniteMeasure μ
⊢ IsFiniteMeasure μ

Tactic:
rw [integral_eq_integral_pos_part_sub_integral_neg_part hfint, sub_nonneg] at hfint'

Premises used: MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
rw : LE.le (α := ℝ) (∫ (ω : α), max (f ω) 0 ∂μ) (∫ (x : α), (↑r : ℝ) ∂μ)
⊢ ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)

Tactic:
rw [← integral_const]

Premises used: MeasureTheory.integral_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ LE.le (α := ℝ) (∫ (ω : α), max (f ω) 0 ∂μ) (∫ (x : α), (↑r : ℝ) ∂μ)

Tactic:
integral_mono_ae hfint.real_toNNReal (integrable_const (r : ℝ)) ?_

Premises used: MeasureTheory.integral_mono_ae, MeasureTheory.Integrable.real_toNNReal, NNReal.toReal, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
refine : (ae μ).EventuallyLE (β := ℝ) (fun (ω : α) ↦ max (f ω) 0) fun (x : α) ↦ (↑r : ℝ)
⊢ LE.le (α := ℝ) (∫ (ω : α), max (f ω) 0 ∂μ) (∫ (x : α), (↑r : ℝ) ∂μ)

Tactic:
refine integral_mono_ae hfint.real_toNNReal (integrable_const (r : ℝ)) ?_

Premises used: MeasureTheory.integral_mono_ae, MeasureTheory.Integrable.real_toNNReal, NNReal.toReal, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
ω : α
hω : f ω ≤ (↑r : ℝ)
⊢ max (f ω) 0 ≤ (↑r : ℝ)

Tactic:
Real.toNNReal_le_iff_le_coe.2 hω

Premises used: Iff.mpr, Real.toNNReal_le_iff_le_coe, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ f ω ≤ (↑r : ℝ)) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ LE.le (α := ℝ) ((fun (ω : α) ↦ max (f ω) 0) x) ((fun (x : α) ↦ (↑r : ℝ)) x)) x} x}
      a
h₁ h₂ : ∀ (ω : α) (hω : f ω ≤ (↑r : ℝ)), max (f ω) 0 ≤ (↑r : ℝ)
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (ω : α) ↦ max (f ω) 0) fun (x : α) ↦ (↑r : ℝ)

Tactic:
filter_upwards [hf] with ω hω using Real.toNNReal_le_iff_le_coe.2 hω
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)

Tactic:
have hposbdd : ∫ ω, max (f ω) 0 ∂μ ≤ μ.real Set.univ • (r : ℝ) := by
    rw [← integral_const]
    refine integral_mono_ae hfint.real_toNNReal (integrable_const (r : ℝ)) ?_
    filter_upwards [hf] with ω hω using Real.toNNReal_le_iff_le_coe.2 hω
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞) ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
pos :
  HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ ENNReal.toReal 1 ∂μ) (ENNReal.toReal 1)⁻¹ ≤
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)).toReal
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)

Tactic:
rw [MemLp.eLpNorm_eq_integral_rpow_norm one_ne_zero ENNReal.one_ne_top
      (memLp_one_iff_integrable.2 hfint),
    ENNReal.ofReal_le_iff_le_toReal (by finiteness)]

Premises used: Iff.mpr, ENNReal.ofReal_le_iff_le_toReal, MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm, one_ne_zero, MeasureTheory.memLp_one_iff_integrable, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
pos :
  ∫ (a : α), (↑(f a).toNNReal : ℝ) + (↑(-f a).toNNReal : ℝ) ∂μ ≤
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)).toReal
⊢ HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ ENNReal.toReal 1 ∂μ) (ENNReal.toReal 1)⁻¹ ≤
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)).toReal

Tactic:
simp_rw [ENNReal.toReal_one, _root_.inv_one, Real.rpow_one, Real.norm_eq_abs, ←
    max_zero_add_max_neg_zero_eq_abs_self, ← Real.coe_toNNReal']

Premises used: inv_one, ENNReal.toReal_one, Real.coe_toNNReal', max_zero_add_max_neg_zero_eq_abs_self, Real.rpow_one, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
pos :
  HAdd.hAdd (α := ℝ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) ≤
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)).toReal
pos₁ : Integrable (ε := ℝ) (fun (a : α) ↦ (↑(-f a).toNNReal : ℝ)) μ
⊢ ∫ (a : α), (↑(f a).toNNReal : ℝ) + (↑(-f a).toNNReal : ℝ) ∂μ ≤
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)).toReal

Tactic:
rw [integral_add hfint.real_toNNReal]

Premises used: MeasureTheory.Integrable.real_toNNReal, MeasureTheory.integral_add