awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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 =ᶠ[ae μ] 0
have hf₁ : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
Tactic: norm_cast at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
have rw : Eq (α := ℝ) (∫ (a : α), f a ∂μ) 0
Tactic: rw [integral_neg, neg_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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
⊢ f =ᶠ[ae μ] 0
have hnegf : 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'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ f =ᶠ[ae μ] 0
have pos : ∀ (this : -f =ᶠ[ae μ] 0), f =ᶠ[ae μ] 0
Tactic: have := (integral_eq_zero_iff_of_nonneg_ae ?_ hfint.neg).1 hnegf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ f =ᶠ[ae μ] 0
have pos₁ : 0 ≤ᶠ[ae μ] -f
Tactic: have := (integral_eq_zero_iff_of_nonneg_ae ?_ hfint.neg).1 hnegf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ f =ᶠ[ae μ] 0
have h : ∀ (ω : α) (hω : (-f) ω = 0 ω), f ω = 0 ω
Tactic: filter_upwards [this] with ω hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 ω
⊢ f ω = 0 ω
have h : ∀ (hω : -f ω = 0 ω), f ω = 0 ω
Tactic: rwa [Pi.neg_apply, Pi.zero_apply, neg_eq_zero] at hω
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 ω
⊢ f ω = 0 ω
have h₁ : ∀ (hω : -f ω = 0), f ω = 0 ω
Tactic: rwa [Pi.neg_apply, Pi.zero_apply, neg_eq_zero] at hω
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 ω
⊢ f ω = 0 ω
have h₂ : ∀ (hω : f ω = 0), f ω = 0 ω
Tactic: rwa [Pi.neg_apply, Pi.zero_apply, neg_eq_zero] at hω
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ 0 ≤ᶠ[ae μ] -f
have h : ∀ (ω : α) (hω : f ω ≤ 0), 0 ω ≤ (-f) ω
Tactic: filter_upwards [hf] with ω hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ 0 ω ≤ (-f) ω
have h : 0 ≤ (-f) ω
Tactic: rwa [Pi.zero_apply, Pi.neg_apply, Right.nonneg_neg_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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) ω
⊢ 0 ω ≤ (-f) ω
have h₁ : 0 ≤ -f ω
Tactic: rwa [Pi.zero_apply, Pi.neg_apply, Right.nonneg_neg_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have pos : ∀ (hμ : IsFiniteMeasure μ),
  eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
Tactic: by_cases hμ : IsFiniteMeasure μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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∞)
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have neg : ∀ (hμ : ¬IsFiniteMeasure μ),
  eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
Tactic: by_cases hμ : IsFiniteMeasure μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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∞)
have by_contra : ∀ (hμ' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)), False
Tactic: by_contra hμ'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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 μ
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have this : 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μ')
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have neg : eLpNorm f 1 μ ≤ ∞
Tactic: rw [this, ENNReal.mul_top', if_neg, ENNReal.top_mul', if_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 μ ≤ ∞
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have neg₁ : ¬(↑r : ℝ≥0∞) = 0
Tactic: rw [this, ENNReal.mul_top', if_neg, ENNReal.top_mul', if_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have neg₂ : ¬Eq (α := ℝ≥0∞) 2 0
Tactic: rw [this, ENNReal.mul_top', if_neg, ENNReal.top_mul', if_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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 μ
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have hfint'₁ : 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'
Cleared hypotheses: hfint', hf, hr, hμ, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 : ℝ)
have rw : LE.le (α := ℝ) (∫ (ω : α), max (f ω) 0 ∂μ) (∫ (x : α), (↑r : ℝ) ∂μ)
Tactic: rw [← integral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 : ℝ) ∂μ)
have refine : (ae μ).EventuallyLE (β := ℝ) (fun (ω : α) ↦ max (f ω) 0) fun (x : α) ↦ (↑r : ℝ)
Tactic: refine integral_mono_ae hfint.real_toNNReal (integrable_const (r : ℝ)) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 μ
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (ω : α) ↦ max (f ω) 0) fun (x : α) ↦ (↑r : ℝ)
have 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
Tactic: filter_upwards [hf] with ω hω using Real.toNNReal_le_iff_le_coe.2 hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (ω : α) ↦ max (f ω) 0) fun (x : α) ↦ (↑r : ℝ)
have h₁ : ∀ (a : α), f a ≤ (↑r : ℝ) → max (f a) 0 ≤ (↑r : ℝ)
Tactic: filter_upwards [hf] with ω hω using Real.toNNReal_le_iff_le_coe.2 hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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 μ
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have hposbdd : ∫ (ω : α), 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ω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 : ℝ)
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)
have 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
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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 : ℝ)
⊢ 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
have pos : ∫ (a : α), (↑(f a).toNNReal : ℝ) + (↑(-f a).toNNReal : ℝ) ∂μ ≤
  (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']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 : ℝ)
⊢ ∫ (a : α), (↑(f a).toNNReal : ℝ) + (↑(-f a).toNNReal : ℝ) ∂μ ≤
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)).toReal
have 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
Tactic: rw [integral_add hfint.real_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
⊢ ∫ (a : α), (↑(f a).toNNReal : ℝ) + (↑(-f a).toNNReal : ℝ) ∂μ ≤
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)).toReal
have pos₁ : Integrable (ε := ℝ) (fun (a : α) ↦ (↑(-f a).toNNReal : ℝ)) μ
Tactic: rw [integral_add hfint.real_toNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 : ℝ)
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), (↑(f a).toNNReal : ℝ) ∂μ) (∫ (a : α), (↑(-f a).toNNReal : ℝ) ∂μ) ≤
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * (↑r : ℝ≥0∞)).toReal
have pos : HAdd.hAdd (α := ℝ) (∫ (a : α), max (f a) 0 ∂μ) (∫ (a : α), max (-f a) 0 ∂μ) ≤
  2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
Tactic: simp only [Real.coe_toNNReal', ENNReal.toReal_mul, ENNReal.coe_toReal,
      toReal_ofNat] at hfint' ⊢
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), max (-f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), max (f a) 0 ∂μ) (∫ (a : α), max (-f a) 0 ∂μ) ≤
    2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
have pos : HAdd.hAdd (α := ℝ) (∫ (a : α), max (f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ) ≤
  2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
Tactic: grw [hfint']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), max (-f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), max (f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ) ≤
    2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
have pos : HMul.hMul (α := ℝ) 2 (∫ (a : α), max (f a) 0 ∂μ) ≤ 2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
Tactic: rwa [← two_mul, mul_assoc, mul_le_mul_iff_right₀ (two_pos : (0 : ℝ) < 2)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), max (-f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
pos : HMul.hMul (α := ℝ) 2 (∫ (a : α), max (f a) 0 ∂μ) ≤ 2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), max (f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ) ≤
    2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
have pos₁ : HMul.hMul (α := ℝ) 2 (∫ (a : α), max (f a) 0 ∂μ) ≤ 2 * (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ))
Tactic: rwa [← two_mul, mul_assoc, mul_le_mul_iff_right₀ (two_pos : (0 : ℝ) < 2)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) (∫ (a : α), max (-f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r : ℝ)
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • (↑r : ℝ)
pos : HMul.hMul (α := ℝ) 2 (∫ (a : α), max (f a) 0 ∂μ) ≤ 2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
pos₁ :
  HMul.hMul (α := ℝ) 2 (∫ (a : α), max (f a) 0 ∂μ) ≤ 2 * (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ))
⊢ HAdd.hAdd (α := ℝ) (∫ (a : α), max (f a) 0 ∂μ) (∫ (a : α), max (f a) 0 ∂μ) ≤
    2 * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
have pos₂ : ∫ (a : α), max (f a) 0 ∂μ ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) * (↑r : ℝ)
Tactic: rwa [← two_mul, mul_assoc, mul_le_mul_iff_right₀ (two_pos : (0 : ℝ) < 2)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
⊢ eLpNorm f 1 μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (2 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) * ENNReal.ofReal r
have refine : ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r.toNNReal : ℝ)
Tactic: refine eLpNorm_one_le_of_le hfint hfint' ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ (↑r.toNNReal : ℝ)
have simp : ∀ᵐ (ω : α) ∂μ, f ω ≤ r ∨ f ω ≤ 0
Tactic: simp only [Real.coe_toNNReal', le_max_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ r ∨ f ω ≤ 0
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ f ω ≤ r) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ f ω ≤ r ∨ f ω ≤ 0) x} x}
    a
Tactic: filter_upwards [hf] with ω hω using Or.inl hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : LE.le (α := ℝ) 0 (∫ (x : α), f x ∂μ)
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ f ω ≤ r) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (ω : α) ↦ f ω ≤ r ∨ f ω ≤ 0) x} x}
      a
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ r ∨ f ω ≤ 0
have h₁ : ∀ (a : α), f a ≤ r → f a ≤ r ∨ f a ≤ 0
Tactic: filter_upwards [hf] with ω hω using Or.inl hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
Goal:
X : Type u_1
E : Type u_3
F : Type u_4
inst : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜' F
inst_7 : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst_8 : RingHomIsometric σ
L : E →SL[σ] F
⊢ Continuous (Y := F) fun (φ : ↥(Lp E 1 μ)) ↦ ∫ (x : X), (L : (a : E) → F) ((↑(↑φ : X →ₘ[μ] E) : X → E) x) ∂μ
have rw : Continuous (Y := F) fun (x : ↥(Lp E 1 μ)) ↦
  ∫ (x_1 : X), (↑(↑(compLp.{u_1, u_3, u_4, u_6, u_7} (𝕜 := 𝕜) (𝕜' := 𝕜') (σ := σ) L x) : X →ₘ[μ] F) : X → F) x_1 ∂μ
Tactic: rw [← funext L.integral_compLp]