awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 μ < ε
⊢ ∃ (φ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0),
        (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
have hs : Set.Nonempty.{u_1} (α := α →ₛ ℝ≥0) fun (φ : α →ₛ ℝ≥0) ↦ ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
Tactic: erw [ENNReal.biSup_add] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
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 μ) +
      ε
⊢ ∃ (φ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0),
        (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
have 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 μ + ε)
Tactic: erw [ENNReal.biSup_add] at this <;> [skip; exact ⟨0, fun x => zero_le⟩]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
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 μ + ε)
⊢ ∃ (φ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0),
        (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
have 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
Tactic: simp_rw [lt_iSup_iff, iSup_lt_iff, iSup_le_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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
⊢ ∃ (φ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0),
        (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
have 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 μ < ε
Tactic: rcases this with ⟨φ, hle : ∀ x, ↑(φ x) ≤ f x, b, hbφ, hb⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 μ < ε
have refine : ∀ (ψ : α →ₛ ℝ≥0) (hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
  (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
Tactic: refine ⟨φ, hle, fun ψ hψ => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
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 μ < ε
have this : (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
Tactic: have : (map (↑) φ).lintegral μ ≠ ∞ := ne_top_of_le_ne_top h (by exact le_iSup₂ (α := ℝ≥0∞) φ hle)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 μ < ε
have rw : (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 μ + ε
have refine : ∀ (x : α),
  (↑((φ + (ψ - φ) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ max (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞)
Tactic: refine (hb _ fun x => le_trans ?_ (max_le (hle x) (hψ x))).trans_lt hbφ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 : α
⊢ (↑((φ + (ψ - φ) : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ max (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞)
have simp : (↑(max ((φ : (a : α) → ℝ≥0) x) ((ψ : (a : α) → ℝ≥0) x)) : ℝ≥0∞) ≤
  (↑(max ((φ : (a : α) → ℝ≥0) x) ((ψ : (a : α) → ℝ≥0) x)) : ℝ≥0∞)
Tactic: simp only [add_apply, sub_apply, add_tsub_eq_max]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
f : ι → α → ℝ≥0∞
⊢ ⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), ⨆ (i : ι), f i a ∂μ
have simp : ⨆ (i : ι), ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), (⨆ (i : ι), f i) a ∂μ
Tactic: simp only [← iSup_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
⊢ ⨆ (i : ι), ⨆ (j : ι' i), ∫⁻ (a : α), f i j a ∂μ ≤ ∫⁻ (a : α), ⨆ (i : ι), ⨆ (j : ι' i), f i j a ∂μ
have h : ∀ (a : α), Eq (α := ℝ≥0∞) (⨆ (i : ι), ⨆ (j : ι' i), f i j a) ((⨆ (i : ι), ⨆ (j : ι' i), f i j) a)
Tactic: convert! (monotone_lintegral μ).le_map_iSup₂ f with a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
f : ι → α → ℝ≥0∞
⊢ ∫⁻ (a : α), ⨅ (i : ι), f i a ∂μ ≤ ⨅ (i : ι), ∫⁻ (a : α), f i a ∂μ
have simp : ∫⁻ (a : α), (⨅ (i : ι), f i) a ∂μ ≤ ⨅ (i : ι), ∫⁻ (a : α), f i a ∂μ
Tactic: simp only [← iInf_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
⊢ ∫⁻ (a : α), ⨅ (i : ι), ⨅ (h : ι' i), f i h a ∂μ ≤ ⨅ (i : ι), ⨅ (h : ι' i), ∫⁻ (a : α), f i h a ∂μ
have h : ∀ (a : α), Eq (α := ℝ≥0∞) (⨅ (i : ι), ⨅ (h : ι' i), f i h a) ((⨅ (i : ι), ⨅ (j : ι' i), f i j) a)
Tactic: convert! (monotone_lintegral μ).map_iInf₂_le f with a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
have 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 ∂μ
Tactic: rcases exists_measurable_superset_of_null h with ⟨t, hts, ht, ht0⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
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∞)
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
have this : ∀ᵐ (x : α) ∂μ, x ∉ t
Tactic: have : ∀ᵐ x ∂μ, x ∉ t := measure_eq_zero_iff_ae_notMem.1 ht0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
have 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 μ)
Tactic: rw [lintegral, lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 μ)
have 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
Tactic: refine iSup₂_le fun s hfs ↦ le_iSup₂_of_le (s.restrict tᶜ) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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
⊢ 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 μ)
have refine_2 : ∀ (s : α →ₛ ℝ≥0∞) (hfs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
  s.lintegral μ ≤ (s.restrict tᶜ).lintegral μ
Tactic: refine iSup₂_le fun s hfs ↦ le_iSup₂_of_le (s.restrict tᶜ) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a) ((s.restrict tᶜ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((fun (a : α) ↦ g a) a : ℝ≥0∞)
have pos : ∀ (h : a ∈ t),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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∞)
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a) ((s.restrict tᶜ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((fun (a : α) ↦ g a) a : ℝ≥0∞)
have neg : ∀ (h : a ∉ t),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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∞)
have neg : (s : (a : α) → ℝ≥0∞) a ≤ g a
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
have rcases : ∀ (f' : α → ℝ≥0∞) (hf'm : Measurable f') (hle : f' ≤ f) (hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ),
  ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
Tactic: rcases exists_measurable_le_lintegral_eq (μ.restrict s) f with ⟨f', hf'm, hle, hf'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
have rw : ∫⁻ (a : α) in s, f' a ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
Tactic: rw [hf']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∫⁻ (a : α) in s, f' a ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
have h : ∀ᵐ (a : α) ∂μ.restrict s, f' a ≤ g a
Tactic: apply lintegral_mono_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∀ᵐ (a : α) ∂μ.restrict s, f' a ≤ g a
have h : ∀ᵐ (x : α) ∂μ, x ∈ s → f' x ≤ g x
Tactic: rw [ae_restrict_iff₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f' x ≤ g x
⊢ ∀ᵐ (a : α) ∂μ.restrict s, f' a ≤ g a
have h₁ : NullMeasurableSet {x : α | f' x ≤ g x} (μ.restrict s)
Tactic: rw [ae_restrict_iff₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ x ∈ s, f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ ∫⁻ (x : α) in s, f x ∂μ
have calc : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ x ∈ s, f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
  ∫⁻ (y : α) in s, ⨅ x ∈ s, f x ∂μ
Tactic: calc (⨅ x ∈ s, f x) * μ s
  _ = ∫⁻ y in s, ⨅ x ∈ s, f x ∂μ := by simp
  _ ≤ ∫⁻ x in s, f x ∂μ := setLIntegral_mono' hs fun x hx ↦ iInf₂_le x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨆ x ∈ s, f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have calc : ∫⁻ (y : α) in s, ⨆ x ∈ s, f x ∂μ =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨆ x ∈ s, f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: calc ∫⁻ x in s, f x ∂μ
  _ ≤ ∫⁻ y in s, ⨆ x ∈ s, f x ∂μ :=
    setLIntegral_mono' hs fun x hx ↦ le_iSup₂ (f := fun x _ ↦ f x) x hx
  _ = (⨆ x ∈ s, f x) * μ s := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
h : s =ᶠ[ae μ] t
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
have rw : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
Tactic: rw [Measure.restrict_congr_set h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
have rw : f =ᶠ[ae (μ.restrict s)] g
Tactic: rw [lintegral_congr_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0
have refine : ∀ (h : ∫⁻ (a : α), f a ∂μ = 0), f =ᶠ[ae μ] 0
Tactic: refine ⟨fun h ↦ ?_, lintegral_eq_zero_of_ae_eq_zero⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
have by_contra! : ∀ (h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)), False
Tactic: by_contra! h'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False
have refine : HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ≤ ∫⁻ (a : α), f a ∂μ
Tactic: refine ((ENNReal.mul_pos εpos.ne' h').trans_le ?_).ne' h