awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 μ) +
      ε
⊢ Set.Nonempty.{u_1} (α := α →ₛ ℝ≥0) fun (φ : α →ₛ ℝ≥0) ↦ ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x

Tactic:
⟨0, fun x => zero_le⟩

Premises used: zero_le, Set.Nonempty, Exists.intro, OfNat.ofNat
-- 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 μ) +
      ε
⊢ Set.Nonempty.{u_1} (α := α →ₛ ℝ≥0) fun (φ : α →ₛ ℝ≥0) ↦ ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x

Tactic:
exact ⟨0, fun x => zero_le⟩
-- 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 μ) +
      ε
⊢ 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 μ + ε)

Tactic:
erw [ENNReal.biSup_add] at this <;> [skip; exact ⟨0, fun x => zero_le⟩]

Premises used: ENNReal.biSup_add
-- 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 :
  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 μ + ε)
⊢ ∃ (i : α →ₛ ℝ≥0) (_ :
    Membership.mem (γ := Set (α →ₛ ℝ≥0)) (fun (φ : α →ₛ ℝ≥0) ↦ ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) i),
    ∃ b < (SimpleFunc.map ofNNReal i).lintegral μ + ε,
      ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
        (SimpleFunc.map ofNNReal i).lintegral μ ≤ b

Tactic:
simp_rw [lt_iSup_iff, iSup_lt_iff, iSup_le_iff] at this

Premises used: iSup_le_iff, iSup_lt_iff, lt_iSup_iff
-- 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 :
  ∃ (i : α →ₛ ℝ≥0) (_ :
    Membership.mem (γ := Set (α →ₛ ℝ≥0)) (fun (φ : α →ₛ ℝ≥0) ↦ ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) i),
    ∃ b < (SimpleFunc.map ofNNReal i).lintegral μ + ε,
      ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
        (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
rcases :
  ∀ (φ : α →ₛ ℝ≥0) (hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) (b : ℝ≥0∞)
    (hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε)
    (hb :
      ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
        (SimpleFunc.map ofNNReal i).lintegral μ ≤ b),
    ∃ (φ : α →ₛ ℝ≥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:
rcases this with ⟨φ, hle : ∀ x, ↑(φ x) ≤ f x, b, hbφ, hb⟩
-- 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
hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
⊢ ∃ (φ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0),
        (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
⟨φ, hle, fun ψ hψ => ?_⟩

Premises used: And.intro, Exists.intro
-- 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
hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
refine :
  ∀ (ψ : α →ₛ ℝ≥0) (hψ : ∀ (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:
refine ⟨φ, hle, fun ψ 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
φ : α →ₛ ℝ≥0
hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal φ).lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
le_iSup₂ (α := ℝ≥0∞) φ hle

Premises used: le_iSup₂
-- 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
hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal φ).lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
exact le_iSup₂ (α := ℝ≥0∞) φ hle

Premises used: le_iSup₂
-- 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
hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞

Tactic:
have : (map (↑) φ).lintegral μ ≠ ∞ := ne_top_of_le_ne_top h (by exact le_iSup₂ (α := ℝ≥0∞) φ hle)
-- 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
hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
rw : (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral μ < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
⊢ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
rw [← ENNReal.add_lt_add_iff_left this, ← add_lintegral, ← SimpleFunc.map_add @ENNReal.coe_add]

Premises used: MeasureTheory.SimpleFunc.map_add, ENNReal.add_lt_add_iff_left, ENNReal.coe_add, MeasureTheory.SimpleFunc.add_lintegral
-- 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
hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
⊢ (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral μ < (SimpleFunc.map ofNNReal φ).lintegral μ + ε

Tactic:
(hb _ fun x => le_trans ?_ (max_le (hle x) (hψ x))).trans_lt hbφ

Premises used: max_le, LE.le.trans_lt, le_trans
-- 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
hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
refine :
  ∀ (x : α),
    (↑((φ + (ψ - φ) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤
      max (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞)
⊢ (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral μ < (SimpleFunc.map ofNNReal φ).lintegral μ + ε

Tactic:
refine (hb _ fun x => le_trans ?_ (max_le (hle x) (hψ x))).trans_lt hbφ

Premises used: max_le, LE.le.trans_lt, le_trans
-- 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
hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
x : α
simp :
  (↑(max ((φ : (a : α) → ℝ≥0) x) ((ψ : (a : α) → ℝ≥0) x)) : ℝ≥0∞) ≤
    (↑(max ((φ : (a : α) → ℝ≥0) x) ((ψ : (a : α) → ℝ≥0) x)) : ℝ≥0∞)
⊢ (↑((φ + (ψ - φ) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ max (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞)

Tactic:
simp only [add_apply, sub_apply, add_tsub_eq_max]

Premises used: MeasureTheory.SimpleFunc.sub_apply, MeasureTheory.SimpleFunc.add_apply, add_tsub_eq_max
-- 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
hle : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
b : ℝ≥0∞
hbφ : b < (SimpleFunc.map ofNNReal φ).lintegral μ + ε
hb :
  ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal i).lintegral μ ≤ b
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
x : α
⊢ (↑(max ((φ : (a : α) → ℝ≥0) x) ((ψ : (a : α) → ℝ≥0) x)) : ℝ≥0∞) ≤
    (↑(max ((φ : (a : α) → ℝ≥0) x) ((ψ : (a : α) → ℝ≥0) x)) : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
f : ι → α → ℝ≥0∞
simp : ⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), (⨆ (i : ι), f i) a ∂μ
⊢ ⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), ⨆ (i : ι), f i a ∂μ

Tactic:
simp only [← iSup_apply]

Premises used: iSup_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
f : ι → α → ℝ≥0∞
⊢ ⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), (⨆ (i : ι), f i) a ∂μ

Tactic:
(monotone_lintegral μ).le_map_iSup

Premises used: Monotone.le_map_iSup, MeasureTheory.monotone_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
f : ι → α → ℝ≥0∞
⊢ ⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), (⨆ (i : ι), f i) a ∂μ

Tactic:
exact (monotone_lintegral μ).le_map_iSup

Premises used: Monotone.le_map_iSup, MeasureTheory.monotone_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
⊢ ⨆ (i : ι), ⨆ (j : ι' i), lintegral μ (f i j) ≤ lintegral μ (⨆ (i : ι), ⨆ (j : ι' i), f i j)

Tactic:
(monotone_lintegral μ).le_map_iSup₂ f

Premises used: Monotone.le_map_iSup₂, MeasureTheory.monotone_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
h : ∀ (a : α), Eq (α := ℝ≥0∞) (⨆ (i : ι), ⨆ (j : ι' i), f i j a) ((⨆ (i : ι), ⨆ (j : ι' i), f i j) a)
⊢ ⨆ (i : ι), ⨆ (j : ι' i), ∫⁻ (a : α), f i j a ∂μ ≤ ∫⁻ (a : α), ⨆ (i : ι), ⨆ (j : ι' i), f i j a ∂μ

Tactic:
convert! (monotone_lintegral μ).le_map_iSup₂ f with a

Premises used: Monotone.le_map_iSup₂, MeasureTheory.monotone_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ι), ⨆ (j : ι' i), f i j a) ((⨆ (i : ι), ⨆ (j : ι' i), f i j) a)

Tactic:
simp only [iSup_apply]

Premises used: iSup_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
f : ι → α → ℝ≥0∞
simp : ∫⁻ (a : α), (⨅ (i : ι), f i) a ∂μ ≤ ⨅ (i : ι), ∫⁻ (a : α), f i a ∂μ
⊢ ∫⁻ (a : α), ⨅ (i : ι), f i a ∂μ ≤ ⨅ (i : ι), ∫⁻ (a : α), f i a ∂μ

Tactic:
simp only [← iInf_apply]

Premises used: iInf_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
f : ι → α → ℝ≥0∞
⊢ ∫⁻ (a : α), (⨅ (i : ι), f i) a ∂μ ≤ ⨅ (i : ι), ∫⁻ (a : α), f i a ∂μ

Tactic:
(monotone_lintegral μ).map_iInf_le

Premises used: Monotone.map_iInf_le, MeasureTheory.monotone_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
f : ι → α → ℝ≥0∞
⊢ ∫⁻ (a : α), (⨅ (i : ι), f i) a ∂μ ≤ ⨅ (i : ι), ∫⁻ (a : α), f i a ∂μ

Tactic:
exact (monotone_lintegral μ).map_iInf_le

Premises used: Monotone.map_iInf_le, MeasureTheory.monotone_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
⊢ lintegral μ (⨅ (i : ι), ⨅ (j : ι' i), f i j) ≤ ⨅ (i : ι), ⨅ (j : ι' i), lintegral μ (f i j)

Tactic:
(monotone_lintegral μ).map_iInf₂_le f

Premises used: MeasureTheory.monotone_lintegral, Monotone.map_iInf₂_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
h : ∀ (a : α), Eq (α := ℝ≥0∞) (⨅ (i : ι), ⨅ (h : ι' i), f i h a) ((⨅ (i : ι), ⨅ (j : ι' i), f i j) a)
⊢ ∫⁻ (a : α), ⨅ (i : ι), ⨅ (h : ι' i), f i h a ∂μ ≤ ⨅ (i : ι), ⨅ (h : ι' i), ∫⁻ (a : α), f i h a ∂μ

Tactic:
convert! (monotone_lintegral μ).map_iInf₂_le f with a

Premises used: MeasureTheory.monotone_lintegral, Monotone.map_iInf₂_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ Eq (α := ℝ≥0∞) (⨅ (i : ι), ⨅ (h : ι' i), f i h a) ((⨅ (i : ι), ⨅ (j : ι' i), f i j) a)

Tactic:
simp only [iInf_apply]

Premises used: iInf_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
rcases :
  ∀ (t : Set α) (hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t) (ht : MeasurableSet t)
    (ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)), ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ

Tactic:
rcases exists_measurable_superset_of_null h with ⟨t, hts, ht, ht0⟩

Premises used: MeasureTheory.exists_measurable_superset_of_null
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, x ∉ t

Tactic:
have : ∀ᵐ x ∂μ, x ∉ t := measure_eq_zero_iff_ae_notMem.1 ht0
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
rw :
  LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ g a), g_1.lintegral μ)
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ

Tactic:
rw [lintegral, lintegral]

Premises used: MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ g a), g_1.lintegral μ)

Tactic:
iSup₂_le fun s hfs ↦ le_iSup₂_of_le (s.restrict tᶜ) ?_ ?_

Premises used: iSup₂_le, Compl.compl, MeasureTheory.SimpleFunc.restrict, le_iSup₂_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
refine_1 :
  ∀ (s : α →ₛ ℝ≥0∞) (hfs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
    LE.le (α := (a : α) → ℝ≥0∞) (⇑(s.restrict tᶜ) : (a : α) → ℝ≥0∞) fun (a : α) ↦ g a
refine_2 :
  ∀ (s : α →ₛ ℝ≥0∞) (hfs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
    s.lintegral μ ≤ (s.restrict tᶜ).lintegral μ
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ g a), g_1.lintegral μ)

Tactic:
refine iSup₂_le fun s hfs ↦ le_iSup₂_of_le (s.restrict tᶜ) ?_ ?_

Premises used: iSup₂_le, le_iSup₂_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
a : α
pos :
  ∀ (h : a ∈ t),
    LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a) ((s.restrict tᶜ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((fun (a : α) ↦ g a) a : ℝ≥0∞)
neg :
  ∀ (h : a ∉ t),
    LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a) ((s.restrict tᶜ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((fun (a : α) ↦ g a) a : ℝ≥0∞)
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a) ((s.restrict tᶜ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((fun (a : α) ↦ g a) a : ℝ≥0∞)

Tactic:
by_cases h : a ∈ t
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h_1 : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
a : α
h : a ∈ t
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a) ((s.restrict tᶜ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((fun (a : α) ↦ g a) a : ℝ≥0∞)

Tactic:
simp only [restrict_apply s ht.compl, mem_compl_iff, h, not_true, not_false_eq_true,
        indicator_of_notMem, zero_le, not_false_eq_true, indicator_of_mem]

Premises used: zero_le, MeasurableSet.compl, Set.indicator_of_mem, MeasureTheory.SimpleFunc.restrict_apply, not_true, Set.indicator_of_notMem, not_false_eq_true, Set.mem_compl_iff