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 α
s : Set α
⊢ ∫⁻ (x : α) in s, 1 ∂μ = (μ : (a : Set α) → ℝ≥0∞) s
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
Tactic: rw [setLIntegral_const, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∫⁻ (x : α) in s, 1 ∂μ = (μ : (a : Set α) → ℝ≥0∞) s
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [setLIntegral_const, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (y : α), ⨅ (x : α), f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
have hfg : ∀ (x : α), ⨅ (x : α), f x ≤ f x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ ∫⁻ (x : α), f x ∂μ
have calc : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
  ∫⁻ (y : α), ⨅ (x : α), f x ∂μ
Tactic: calc (⨅ x, f x) * μ .univ
  _ = ∫⁻ y, ⨅ x, f x ∂μ := by simp
  _ ≤ ∫⁻ x, f x ∂μ := by gcongr; exact iInf_le _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
calc :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    ∫⁻ (y : α), ⨅ (x : α), f x ∂μ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ ∫⁻ (x : α), f x ∂μ
have calc₁ : ∫⁻ (y : α), ⨅ (x : α), f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
Tactic: calc (⨅ x, f x) * μ .univ
  _ = ∫⁻ y, ⨅ x, f x ∂μ := by simp
  _ ≤ ∫⁻ x, f x ∂μ := by gcongr; exact iInf_le _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (y : α), ⨆ (x : α), f x ∂μ
have hfg : ∀ (x : α), f x ≤ ⨆ (x : α), f x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨆ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have calc : ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (y : α), ⨆ (x : α), f x ∂μ
Tactic: calc ∫⁻ x, f x ∂μ
  _ ≤ ∫⁻ y, ⨆ x, f x ∂μ := by gcongr; exact le_iSup _ _
  _ = (⨆ x, f x) * μ .univ := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
calc : ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (y : α), ⨆ (x : α), f x ∂μ
⊢ ∫⁻ (x : α), f x ∂μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨆ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have calc₁ : ∫⁻ (y : α), ⨆ (x : α), f x ∂μ =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨆ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: calc ∫⁻ x, f x ∂μ
  _ ≤ ∫⁻ y, ⨆ x, f x ∂μ := by gcongr; exact le_iSup _ _
  _ = (⨆ x, f x) * μ .univ := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
have inl : ∀ (h₀ : ∫⁻ (a : α), f a ∂μ = 0), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
Tactic: rcases eq_or_ne (∫⁻ a, f a ∂μ) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inl : ∀ (h₀ : ∫⁻ (a : α), f a ∂μ = 0), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
have inr : ∀ (h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
Tactic: rcases eq_or_ne (∫⁻ a, f a ∂μ) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
have inr : ∀ (L : ℕ → ℝ≥0∞),
  StrictMono L →
    ∀ (hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)) (hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))),
      ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
Tactic: rcases exists_seq_strictMono_tendsto' h₀.bot_lt with ⟨L, _, hLf, hL_tendsto⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
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 : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
have this : ∀ (n : ℕ), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ L n < ∫⁻ (a : α), g a ∂μ
Tactic: have : ∀ n, ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ L n < ∫⁻ a, g a ∂μ := by
    intro n
    simpa only [← iSup_lintegral_measurable_le_eq_lintegral f, lt_iSup_iff, exists_prop] using
      (hLf n).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ))
this : ∀ (n : ℕ), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ L n < ∫⁻ (a : α), g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
have inr : ∀ (g : (n : ℕ) → α → ℝ≥0∞) (hgm : ∀ (n : ℕ), Measurable (g n)) (hgf : ∀ (n : ℕ), g n ≤ f)
  (hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ),
  ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
Tactic: choose g hgm hgf hLg using 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₀ : ∫⁻ (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 ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
have inr : ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ
Tactic: refine
    ⟨fun x => ⨆ n, g n x, .iSup hgm, fun x => iSup_le fun n => hgf n x, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
have inr₁ : ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ ≤ ∫⁻ (a : α), f a ∂μ
Tactic: refine
    ⟨fun x => ⨆ n, g n x, .iSup hgm, fun x => iSup_le fun n => hgf n x, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 ∂μ
have inr : ∀ (n : ℕ) (x : α), g n x ≤ ⨆ (n : ℕ), g n x
Tactic: refine le_of_tendsto' hL_tendsto fun n => (hLg n).le.trans <| lintegral_mono fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
⊢ ∫⁻ (a : α), f a ∂μ =
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
have 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 μ)
Tactic: rw [lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 μ)
have 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 μ
Tactic: refine
    le_antisymm (iSup₂_le fun φ hφ ↦ ?_) (iSup_mono' fun φ ↦ ⟨φ.map ((↑) : ℝ≥0 → ℝ≥0∞), le_rfl⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥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 μ
have pos : ∀ (h : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)),
  φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
Tactic: by_cases h : ∀ᵐ a ∂μ, φ a ≠ ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 μ
⊢ φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
have neg : ∀ (h : ¬∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)),
  φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
Tactic: by_cases h : ∀ᵐ a ∂μ, φ a ≠ ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
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 φ
⊢ φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
have h₁ : (ae μ).EventuallyEq (β := ℝ≥0∞) (⇑(SimpleFunc.map ofNNReal ψ) : (a : α) → ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞)
Tactic: replace h : ψ.map ((↑) : ℝ≥0 → ℝ≥0∞) =ᵐ[μ] φ := h.mono fun a => ENNReal.coe_toNNReal
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
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∞)
⊢ φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
have this : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
Tactic: have : ∀ x, ↑(ψ x) ≤ f x := fun x => le_trans ENNReal.coe_toNNReal_le_self (hφ x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
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∞)
⊢ φ.lintegral μ ≤
    ⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ
have h_meas : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 μ
have neg : ∀ (b : ℝ≥0∞) (hb : b < ∞),
  ∃ (i : α →ₛ ℝ≥0),
    b < ⨆ (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ
Tactic: refine le_trans le_top (ge_of_eq <| iSup_eq_top.2 fun b hb => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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 < ∞
⊢ ∃ (i : α →ₛ ℝ≥0),
    b < ⨆ (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ
have 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 μ
Tactic: obtain ⟨n, hn⟩ : ∃ n : ℕ, b < n * μ (φ ⁻¹' {∞}) := exists_nat_mul_gt h_meas (ne_of_lt hb)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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∞)
⊢ ∃ (i : α →ₛ ℝ≥0),
    b < ⨆ (_ : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ
have 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∞) {∞}))) μ
Tactic: use (const α (n : ℝ≥0)).restrict (φ ⁻¹' {∞})
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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∞)
⊢ 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∞) {∞}))) μ
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
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∞)
have h₁ : ∀ (x : α) (hx : Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑φ : (a : α) → ℝ≥0∞) {∞}) x),
  (↑(Function.const α (↑n : ℝ≥0) x) : ℝ≥0∞) ≤ (φ : (a : α) → ℝ≥0∞) x
Tactic: refine ⟨indicator_le fun x hx => le_trans ?_ (hφ _), hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
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
⊢ (↑(Function.const α (↑n : ℝ≥0) x) : ℝ≥0∞) ≤ (φ : (a : α) → ℝ≥0∞) x
have hx₁ : Eq (α := ℝ≥0∞) ((φ : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [mem_preimage, mem_singleton_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (φ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0),
        (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
have 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 μ < ε
Tactic: rw [lintegral_eq_nnreal] at h
Cleared hypotheses: h, ε, 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),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0),
        (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
have 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 μ) +
    ε
Tactic: have := ENNReal.lt_add_right h hε
-- 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 μ) +
      ε
⊢ ∃ (φ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0),
        (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε
have 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 μ < ε
Tactic: erw [ENNReal.biSup_add] at this
Cleared hypotheses: this