-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem eLpNorm_one_le_of_le {r : ℝ≥0} (hfint : Integrable f μ) (hfint' : 0 ≤ ∫ x, f x ∂μ)
    (hf : ∀ᵐ ω ∂μ, f ω ≤ r) : eLpNorm f 1 μ ≤ 2 * μ Set.univ * r

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r

Tactic:
have : μ Set.univ = ∞ := by
  by_contra hμ'
  exact hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')

Result:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : μ univ = ⊤
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
⊢ μ univ = ⊤

Tactic:
by_contra hμ'

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
hμ' : ¬μ univ = ⊤
⊢ False

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ ∫ (a : α), f a ∂μ = 0

Tactic:
exact le_antisymm (integral_nonpos_of_ae hf) hfint'

Result:
no goals

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : r = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
rw [hr] at hf

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑0
hr : r = 0
⊢ f =ᶠ[ae μ] 0

Proof state:
case neg.hnc
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : μ univ = ⊤
⊢ ¬2 = 0

Tactic:
norm_num

Result:
no goals

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), f ω ⊔ 0 ∂μ ≤ (μ univ).toReal • ↑r
⊢ ∫ (a : α), ↑(f a).toNNReal + ↑(-f a).toNNReal ∂μ ≤ (2 * μ univ * ↑r).toReal

Tactic:
rw [integral_add hfint.real_toNNReal]

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), f ω ⊔ 0 ∂μ ≤ (μ univ).toReal • ↑r
⊢ ∫ (a : α), ↑(f a).toNNReal ∂μ + ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ (2 * μ univ * ↑r).toReal

case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), f ω ⊔ 0 ∂μ ≤ (μ univ).toReal • ↑r
⊢ Integrable (fun a => ↑(-f a).toNNReal) μ

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ f =ᶠ[ae μ] 0

Tactic:
have hnegf : ∫ x, -f x ∂μ = 0 := by
  rw [integral_neg, neg_eq_zero]
  exact le_antisymm (integral_nonpos_of_ae hf) hfint'

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
⊢ f =ᶠ[ae μ] 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
hμ' : ¬μ univ = ⊤
⊢ False

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

Result:
no goals

Proof state:
case pos.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
⊢ 0 ≤ᶠ[ae μ] -f

Tactic:
filter_upwards [hf] with ω hω

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
ω : α
hω : f ω ≤ 0
⊢ 0 ω ≤ (-f) ω

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), f ω ⊔ 0 ∂μ ≤ (μ univ).toReal • ↑r
⊢ Integrable (fun a => ↑(-f a).toNNReal) μ

Tactic:
exact hfint.neg.sup (integrable_zero _ _ μ)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ ∫ (x : α), -f x ∂μ = 0

Tactic:
rw [integral_neg, neg_eq_zero]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ ∫ (a : α), f a ∂μ = 0