awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
⊢ f =ᶠ[ae μ] 0
have meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have meas_levels_0 : ∀ ε > 0, μ { x | ε ≤ f x } = 0 := fun ε εpos ↦ by
    by_contra! h'
    refine ((ENNReal.mul_pos εpos.ne' h').trans_le ?_).ne' h
    calc
      _ ≥ ∫⁻ a in {x | ε ≤ f x}, f a ∂μ := setLIntegral_le_lintegral _ _
      _ ≥ ∫⁻ _ in {x | ε ≤ f x}, ε ∂μ :=
        setLIntegral_mono_ae hf.restrict (ae_of_all μ fun _ ↦ id)
      _ = _ := setLIntegral_const _ _
-- 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
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f =ᶠ[ae μ] 0
have obtain : ∀ (u : ℕ → ℝ≥0∞) (bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)) (tu : Tendsto u atTop (𝓝 0)),
  f =ᶠ[ae μ] 0
Tactic: obtain ⟨u, -, bu, tu⟩ := exists_seq_strictAnti_tendsto' (α := ℝ≥0∞) zero_lt_one
-- 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
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | f x ≠ 0} (⋃ (n : ℕ), {x : α | u n ≤ f x})
have h₁ : ∀ (x : α),
  Membership.mem (γ := Set α) {x : α | f x ≠ 0} x ↔ Membership.mem (γ := Set α) (⋃ (n : ℕ), {x : α | u n ≤ f x}) x
Tactic: ext x
-- 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
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
x : α
⊢ Membership.mem (γ := Set α) {x : α | f x ≠ 0} x ↔ Membership.mem (γ := Set α) (⋃ (n : ℕ), {x : α | u n ≤ f x}) x
have h₁ : 0 < f x ↔ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
Tactic: rw [mem_iUnion, mem_setOf_eq, ← pos_iff_ne_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
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
x : α
⊢ 0 < f x ↔ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
have h₁ : ∀ (tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε) (x : α),
  0 < f x ↔ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
Tactic: rw [ENNReal.tendsto_atTop_zero] at tu
Cleared hypotheses: tu, x
-- 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
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
⊢ 0 < f x ↔ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
have h₁ : 0 < f x → ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
Tactic: constructor
-- 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
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
h₁ : 0 < f x → ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
⊢ 0 < f x ↔ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
have h₂ : (∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x) → 0 < f x
Tactic: constructor
-- 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
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
h' : 0 < f x
⊢ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
have h₁ : ∀ (n : ℕ) (hn : ∀ n_1 ≥ n, u n_1 ≤ f x), ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
Tactic: obtain ⟨n, hn⟩ := tu _ 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
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
h' : 0 < f x
n : ℕ
hn : ∀ n_1 ≥ n, u n_1 ≤ f x
w : ℕ
⊢ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
have h₁ : Membership.mem (γ := Set α) {x : α | u n ≤ f x} x
Tactic: use n, hn _ le_rfl
-- 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
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
h' : ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
⊢ 0 < f x
have h₁ : ∀ (n : ℕ) (hn : Membership.mem (γ := Set α) {x : α | u n ≤ f x} x), 0 < f x
Tactic: obtain ⟨n, hn⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
⊢ f =ᶠ[ae μ] 0
have u_union : Eq.{u_1 + 1} (α := Set α) {x : α | f x ≠ 0} (⋃ (n : ℕ), {x : α | u n ≤ f x})
Tactic: have u_union : {x | f x ≠ 0} = ⋃ n, {x | u n ≤ f x} := by
    ext x
    rw [mem_iUnion, mem_setOf_eq, ← pos_iff_ne_zero]
    rw [ENNReal.tendsto_atTop_zero] at tu
    constructor <;> intro h'
    · obtain ⟨n, hn⟩ := tu _ h'; use n, hn _ le_rfl
    · obtain ⟨n, hn⟩ := h'; exact (bu n).1.trans_le hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
u_union : Eq.{u_1 + 1} (α := Set α) {x : α | f x ≠ 0} (⋃ (n : ℕ), {x : α | u n ≤ f x})
⊢ f =ᶠ[ae μ] 0
have res : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), {x : α | u i ≤ f x}) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have res := measure_iUnion_null_iff.mpr fun n ↦ meas_levels_0 _ (bu n).1
-- 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
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
u_union : Eq.{u_1 + 1} (α := Set α) {x : α | f x ≠ 0} (⋃ (n : ℕ), {x : α | u n ≤ f x})
res : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), {x : α | u i ≤ f x}) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f =ᶠ[ae μ] 0
have rwa : ∀ (res : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≠ 0} : ℝ≥0∞) (0 : ℝ≥0∞)), f =ᶠ[ae μ] 0
Tactic: rwa [← u_union] at res
Cleared hypotheses: res
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
⊢ 0 < ∫⁻ (a : α) in s, f a ∂μ ↔ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f ∩ s) : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) ↔
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f ∩ s) : ℝ≥0∞)
Tactic: rw [lintegral_pos_iff_support hf, Measure.restrict_apply (measurableSet_support hf)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f ∩ s) : ℝ≥0∞)
⊢ 0 < ∫⁻ (a : α) in s, f a ∂μ ↔ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f ∩ s) : ℝ≥0∞)
have rw₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f ∩ s) : ℝ≥0∞) ↔
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f ∩ s) : ℝ≥0∞)
Tactic: rw [lintegral_pos_iff_support hf, Measure.restrict_apply (measurableSet_support hf)]
-- 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, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
have rcases : ∀ (ε₂ : ℝ≥0∞) (hε₂0 : 0 < ε₂) (hε₂ε : ε₂ < ε),
  ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
Tactic: rcases exists_between (pos_iff_ne_zero.mpr hε) with ⟨ε₂, hε₂0, hε₂ε⟩
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
⊢ ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
have rcases : ∀ (ε₁ : ℝ≥0∞) (hε₁0 : 0 < ε₁) (hε₁₂ : ε₁ < ε₂),
  ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
Tactic: rcases exists_between hε₂0 with ⟨ε₁, hε₁0, hε₁₂⟩
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
⊢ ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
have rcases : ∀ (φ : α →ₛ ℝ≥0),
  (∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) →
    ∀
      (hφ :
        ∀ (ψ : α →ₛ ℝ≥0),
          (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁),
      ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
Tactic: rcases exists_simpleFunc_forall_lintegral_sub_lt_of_pos h hε₁0.ne' with ⟨φ, _, hφ⟩
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
⊢ ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
have rcases : ∀ (C : ℝ≥0) (hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C),
  ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
Tactic: rcases φ.exists_forall_le with ⟨C, hC⟩
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
⊢ ∃ δ > 0, ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
have right : ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ < ε
Tactic: use (ε₂ - ε₁) / C, ENNReal.div_pos_iff.2 ⟨(tsub_pos_iff_lt.2 hε₁₂).ne', ENNReal.coe_ne_top⟩
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
⊢ ∀ (s : Set α), (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ < ε
have right : ∀ (s : Set α) (hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)), ∫⁻ (x : α) in s, f x ∂μ ≤ ε₂
Tactic: refine fun s hs => lt_of_le_of_lt ?_ hε₂ε
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ε₂
have right : ∀ (i : α →ₛ ℝ≥0) (i_1 : ∀ (x : α), (↑((i : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
  (SimpleFunc.map ofNNReal i).lintegral (μ.restrict s) ≤ ε₂
Tactic: simp only [lintegral_eq_nnreal, iSup_le_iff]
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s)
have rw : (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral (μ.restrict s)
Tactic: rw [← SimpleFunc.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 : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral (μ.restrict s)
have refine : ∀ (x : α),
  LE.le (α := ℝ≥0∞) ((SimpleFunc.map ofNNReal ψ : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
    ((SimpleFunc.map ofNNReal (φ + (ψ - φ)) : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: refine SimpleFunc.lintegral_mono (fun x => ?_) le_rfl
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + ε₁
have bc : (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤ ε₁
Tactic: gcongr
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤ ε₁
have bc : (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s) ≤ (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ
Tactic: refine le_trans ?_ (hφ _ hψ).le
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + ε₁ ≤
    SimpleFunc.lintegral (const α (↑C : ℝ≥0∞)) (μ.restrict s) + ε₁
have bc : SimpleFunc.map ofNNReal φ ≤ const α (↑C : ℝ≥0∞)
Tactic: gcongr
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (↑C : ℝ≥0∞) * ((ε₂ - ε₁) / (↑C : ℝ≥0∞)) + ε₁ ≤ ε₂ - ε₁ + ε₁
have bc : (↑C : ℝ≥0∞) * ((ε₂ - ε₁) / (↑C : ℝ≥0∞)) ≤ ε₂ - ε₁
Tactic: gcongr
-- 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∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
hφ :
  ∀ (ψ : α →ₛ ℝ≥0),
    (∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), (φ : (a : α) → ℝ≥0) x ≤ C
s : Set α
hs : (μ : (a : Set α) → ℝ≥0∞) s < (ε₂ - ε₁) / (↑C : ℝ≥0∞)
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ε₂
have rw : (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤
  (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) + (SimpleFunc.map ofNNReal (ψ - φ)).lintegral (μ.restrict s)
Tactic: calc
    (map (↑) ψ).lintegral (μ.restrict s) ≤
        (map (↑) φ).lintegral (μ.restrict s) + (map (↑) (ψ - φ)).lintegral (μ.restrict s) := by
      rw [← SimpleFunc.add_lintegral, ← SimpleFunc.map_add @ENNReal.coe_add]
      refine SimpleFunc.lintegral_mono (fun x => ?_) le_rfl
      simp only [add_tsub_eq_max, le_max_right, coe_map, Function.comp_apply, SimpleFunc.coe_add,
        SimpleFunc.coe_sub, Pi.add_apply, Pi.sub_apply, ENNReal.coe_max (φ x) (ψ x)]
    _ ≤ (map (↑) φ).lintegral (μ.restrict s) + ε₁ := by
      gcongr
      refine le_trans ?_ (hφ _ hψ).le
      exact SimpleFunc.lintegral_mono le_rfl Measure.restrict_le_self
    _ ≤ (SimpleFunc.const α (C : ℝ≥0∞)).lintegral (μ.restrict s) + ε₁ := by
      gcongr
      exact fun x ↦ ENNReal.coe_le_coe.2 (hC x)
    _ = C * μ s + ε₁ := by
      simp only [← SimpleFunc.lintegral_eq_lintegral, coe_const, lintegral_const,
        Measure.restrict_apply, MeasurableSet.univ, univ_inter, Function.const]
    _ ≤ C * ((ε₂ - ε₁) / C) + ε₁ := by gcongr
    _ ≤ ε₂ - ε₁ + ε₁ := by gcongr; apply mul_div_le
    _ = ε₂ := tsub_add_cancel_of_le hε₁₂.le