awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
inr : ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ
inr₁ : ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ ≤ ∫⁻ (a : α), f a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
refine
    ⟨fun x => ⨆ n, g n x, .iSup hgm, fun x => iSup_le fun n => hgf n x, le_antisymm ?_ ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ

Tactic:
le_of_tendsto' hL_tendsto fun n => (hLg n).le.trans <| lintegral_mono fun x => ?_

Premises used: LT.lt.le, MeasureTheory.lintegral_mono, LE.le.trans, le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
inr : ∀ (n : ℕ) (x : α), g n x ≤ ⨆ (n : ℕ), g n x
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ

Tactic:
refine le_of_tendsto' hL_tendsto fun n => (hLg n).le.trans <| lintegral_mono fun x => ?_

Premises used: LT.lt.le, MeasureTheory.lintegral_mono, LE.le.trans, le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
n : ℕ
x : α
⊢ g n x ≤ ⨆ (n : ℕ), g n x

Tactic:
le_iSup (fun n => g n x) n

Premises used: le_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
n : ℕ
x : α
⊢ g n x ≤ ⨆ (n : ℕ), g n x

Tactic:
exact le_iSup (fun n => g n x) n

Premises used: le_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
⊢ ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
lintegral_mono fun x => iSup_le fun n => hgf n x

Premises used: MeasureTheory.lintegral_mono, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
⊢ ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
exact lintegral_mono fun x => iSup_le fun n => hgf n x

Premises used: MeasureTheory.lintegral_mono, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
rw :
  Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ)
⊢ ∫⁻ (a : α), f a ∂μ =
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
rw [lintegral]

Premises used: MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
⊢ Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ)

Tactic:
le_antisymm (iSup₂_le fun φ hφ ↦ ?_) (iSup_mono' fun φ ↦ ⟨φ.map ((↑) : ℝ≥0 → ℝ≥0∞), le_rfl⟩)

Premises used: iSup₂_le, ENNReal.ofNNReal, le_rfl, iSup_mono', le_antisymm, Exists.intro, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
le_antisymm :
  ∀ (φ : α →ₛ ℝ≥0∞) (hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
    φ.lintegral μ ≤
      ⨆ (φ : α →ₛ ℝ≥0),
        ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
⊢ Eq (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ)

Tactic:
refine
    le_antisymm (iSup₂_le fun φ hφ ↦ ?_) (iSup_mono' fun φ ↦ ⟨φ.map ((↑) : ℝ≥0 → ℝ≥0∞), le_rfl⟩)

Premises used: iSup₂_le, iSup_mono', le_antisymm, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
pos :
  ∀ (h : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)),
    φ.lintegral μ ≤
      ⨆ (φ : α →ₛ ℝ≥0),
        ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
neg :
  ∀ (h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)),
    φ.lintegral μ ≤
      ⨆ (φ : α →ₛ ℝ≥0),
        ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
⊢ φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
by_cases h : ∀ᵐ a ∂μ, φ a ≠ ∞
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (⇑(SimpleFunc.map ofNNReal ψ) : (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞)

Tactic:
replace h : ψ.map ((↑) : ℝ≥0 → ℝ≥0∞) =ᵐ[μ] φ := h.mono fun a => ENNReal.coe_toNNReal
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
h : (ae μ).EventuallyEq (β := ℝ≥0∞) (⇑(SimpleFunc.map ofNNReal ψ) : (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞)
⊢ ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x

Tactic:
have : ∀ x, ↑(ψ x) ≤ f x := fun x => le_trans ENNReal.coe_toNNReal_le_self (hφ x)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
h : (ae μ).EventuallyEq (β := ℝ≥0∞) (⇑(SimpleFunc.map ofNNReal ψ) : (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞)
this : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
le_iSup₂_of_le (φ.map ENNReal.toNNReal) this (ge_of_eq <| lintegral_congr h)

Premises used: MeasureTheory.SimpleFunc.lintegral_congr, ge_of_eq, ENNReal.toNNReal, le_iSup₂_of_le, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
h : (ae μ).EventuallyEq (β := ℝ≥0∞) (⇑(SimpleFunc.map ofNNReal ψ) : (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞)
this : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
exact le_iSup₂_of_le (φ.map ENNReal.toNNReal) this (ge_of_eq <| lintegral_congr h)

Premises used: ge_of_eq, ENNReal.toNNReal, le_iSup₂_of_le, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have h_meas : μ (φ ⁻¹' {∞}) ≠ 0 := mt measure_eq_zero_iff_ae_notMem.1 h
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
le_trans le_top (ge_of_eq <| iSup_eq_top.2 fun b hb => ?_)

Premises used: Iff.mpr, ge_of_eq, iSup_eq_top, le_top, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  ∀ (b : ℝ≥0∞) (hb : b < ∞),
    ∃ (i : α →ₛ ℝ≥0),
      b < ⨆ (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ
⊢ φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
refine le_trans le_top (ge_of_eq <| iSup_eq_top.2 fun b hb => ?_)

Premises used: Iff.mpr, ge_of_eq, iSup_eq_top, le_top, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
b : ℝ≥0∞
hb : b < ∞
⊢ ∃ (n : ℕ),
    b <
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)

Tactic:
exists_nat_mul_gt h_meas (ne_of_lt hb)

Premises used: ENNReal.exists_nat_mul_gt, ne_of_lt
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
b : ℝ≥0∞
hb : b < ∞
neg :
  ∀ (n : ℕ)
    (hn :
      b <
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)),
    ∃ (i : α →ₛ ℝ≥0),
      b < ⨆ (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ
⊢ ∃ (i : α →ₛ ℝ≥0),
    b < ⨆ (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, b < n * μ (φ ⁻¹' {∞}) := exists_nat_mul_gt h_meas (ne_of_lt hb)

Premises used: ENNReal.exists_nat_mul_gt, Set.preimage, Top.top, Singleton.singleton, ne_of_lt, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
b : ℝ≥0∞
hb : b < ∞
n : ℕ
hn :
  b <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)
h₁ :
  b <
    ⨆ (_ :
      ∀ (x : α),
        (↑(((restrict (const α (↑n : ℝ≥0)) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : α →ₛ ℝ≥0) : (a : α) → ℝ≥0)
                x) :
            ℝ≥0∞) ≤
          f x),
      SimpleFunc.lintegral
        (SimpleFunc.map ofNNReal (restrict (const α (↑n : ℝ≥0)) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}))) μ
⊢ ∃ (i : α →ₛ ℝ≥0),
    b < ⨆ (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ

Tactic:
use (const α (n : ℝ≥0)).restrict (φ ⁻¹' {∞})

Premises used: MeasureTheory.SimpleFunc.const, Nat.cast, MeasureTheory.SimpleFunc.restrict, Set.preimage, Top.top, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
b : ℝ≥0∞
hb : b < ∞
n : ℕ
hn :
  b <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)
h₁ :
  (∀ (x : α),
      indicator (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞})
          (fun (x : α) ↦ (↑(Function.const α (↑n : ℝ≥0) x) : ℝ≥0∞)) x ≤
        f x) ∧
    b <
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)
⊢ b <
    ⨆ (_ :
      ∀ (x : α),
        (↑(((restrict (const α (↑n : ℝ≥0)) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : α →ₛ ℝ≥0) : (a : α) → ℝ≥0)
                x) :
            ℝ≥0∞) ≤
          f x),
      SimpleFunc.lintegral
        (SimpleFunc.map ofNNReal (restrict (const α (↑n : ℝ≥0)) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}))) μ

Tactic:
simp only [lt_iSup_iff, exists_prop, coe_restrict, φ.measurableSet_preimage, coe_const,
      ENNReal.coe_indicator, map_coe_ennreal_restrict, SimpleFunc.map_const, ENNReal.coe_natCast,
      restrict_const_lintegral]

Premises used: MeasureTheory.SimpleFunc.restrict_const_lintegral, MeasureTheory.SimpleFunc.map_const, exists_prop, MeasureTheory.SimpleFunc.coe_restrict, MeasureTheory.SimpleFunc.measurableSet_preimage, ENNReal.coe_natCast, MeasureTheory.SimpleFunc.coe_const, ENNReal.coe_indicator, MeasureTheory.SimpleFunc.map_coe_ennreal_restrict, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
b : ℝ≥0∞
hb : b < ∞
n : ℕ
hn :
  b <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)
⊢ (∀ (x : α),
      indicator (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞})
          (fun (x : α) ↦ (↑(Function.const α (↑n : ℝ≥0) x) : ℝ≥0∞)) x ≤
        f x) ∧
    b <
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)

Tactic:
⟨indicator_le fun x hx => le_trans ?_ (hφ _), hn⟩

Premises used: And.intro, Set.indicator_le, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
b : ℝ≥0∞
hb : b < ∞
n : ℕ
hn :
  b <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)
h₁ :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) x),
    (↑(Function.const α (↑n : ℝ≥0) x) : ℝ≥0∞) ≤ (φ : (a : α) → ℝ≥0∞) x
⊢ (∀ (x : α),
      indicator (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞})
          (fun (x : α) ↦ (↑(Function.const α (↑n : ℝ≥0) x) : ℝ≥0∞)) x ≤
        f x) ∧
    b <
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)

Tactic:
refine ⟨indicator_le fun x hx => le_trans ?_ (hφ _), hn⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
b : ℝ≥0∞
hb : b < ∞
n : ℕ
hn :
  b <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) x
⊢ Eq (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [mem_preimage, mem_singleton_iff] at hx

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : LE.le (α := (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
b : ℝ≥0∞
hb : b < ∞
n : ℕ
hn :
  b <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞)
x : α
hx : Eq (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑(Function.const α (↑n : ℝ≥0) x) : ℝ≥0∞) ≤ (φ : (a : α) → ℝ≥0∞) x

Tactic:
simp only [hx, le_top]

Premises used: le_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
rw :
  ∀
    (h :
      Ne (α := ℝ≥0∞)
        (⨆ (φ : α →ₛ ℝ≥0),
          ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ)
        ∞)
    {ε : ℝ≥0∞} (hε : ε ≠ 0),
    ∃ (φ : α →ₛ ℝ≥0),
      (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
        ∀ (ψ : α →ₛ ℝ≥0),
          (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
⊢ ∃ (φ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0),
        (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
rw [lintegral_eq_nnreal] at h

Premises used: MeasureTheory.lintegral_eq_nnreal
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  Ne (α := ℝ≥0∞)
    (⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ)
    ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    (⨆ (φ : α →ₛ ℝ≥0),
        ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ) +
      ε

Tactic:
have := ENNReal.lt_add_right h hε
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  Ne (α := ℝ≥0∞)
    (⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ)
    ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this :
  ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    (⨆ (φ : α →ₛ ℝ≥0),
        ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ) +
      ε
erw :
  ∀
    (this :
      LT.lt (α := ℝ≥0∞)
        (⨆ (φ : α →ₛ ℝ≥0),
          ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ)
        (⨆ (i : α →ₛ ℝ≥0),
          ⨆ (_ :
            Membership.mem (γ := Set (α →ₛ ℝ≥0))
              (fun (φ : α →ₛ ℝ≥0) ↦ ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) i),
            (SimpleFunc.map ofNNReal i).lintegral μ + ε)),
    ∃ (φ : α →ₛ ℝ≥0),
      (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
        ∀ (ψ : α →ₛ ℝ≥0),
          (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
hs : Set.Nonempty.{u_1} (α := α →ₛ ℝ≥0) fun (φ : α →ₛ ℝ≥0) ↦ ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ ∃ (φ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0),
        (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
erw [ENNReal.biSup_add] at this

Premises used: ENNReal.biSup_add