awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ∑' (i : α), (ofNNReal ∘ a) i ≤ (↑c : ℝ≥0∞)
have h : ∑' (i : α), (ofNNReal ∘ a) i = (↑(∑' (i : α), a i) : ℝ≥0∞)
Tactic: convert! ENNReal.coe_le_coe.mpr tsum_le_c
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : ∑' (i : α), a i ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ∑' (i : α), (↑(a i) : ℝ≥0∞) = (↑(∑' (i : α), a i) : ℝ≥0∞)
have h : (↑(∑' (b : α), a b) : ℝ≥0∞) = (↑(∑' (i : α), a i) : ℝ≥0∞)
Tactic: rw [ENNReal.tsum_coe_eq a_summable.hasSum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
f : α → ℝ≥0∞
| ∫⁻ (a : α), f a ∂μ
have rw : ∑' (i : α), ∫⁻ (a : α), f a ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞) (dirac i)
Tactic: rw [← sum_smul_dirac μ, lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ = ∑' (a : α), HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
have conv_lhs : Eq (α := ℝ≥0∞)
  (∑' (i : α),
    ∫⁻ (a : α), f a ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞) (dirac i))
  (∑' (a : α), HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞))
Tactic: conv_lhs => rw [← sum_smul_dirac μ, lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞)
    (∑' (i : α),
      ∫⁻ (a : α), f a ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {i} : ℝ≥0∞) (dirac i))
    (∑' (a : α), HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞))
have e_f : ∀ (a : α),
  ∫⁻ (a : α), f a ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (dirac a) =
    HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞)
Tactic: congr 1 with a : 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
f : α → ℝ≥0∞
s : Set α
hs : s.Countable
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in ⋃ x ∈ s, {x}, f a ∂μ
have rw : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
Tactic: rw [biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∉ s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in insert a s, f x ∂μ =
    HMul.hMul (β := ℝ≥0∞) (f a) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) + ∫⁻ (x : α) in s, f x ∂μ
have rw : Disjoint s {a}
Tactic: rw [← union_singleton, lintegral_union (measurableSet_singleton a), lintegral_singleton,
    add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
inst_2 : Fintype α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = ∑ x : α, HMul.hMul (β := ℝ≥0∞) (f x) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
have rw : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in (↑Finset.univ : Set α), f x ∂μ
Tactic: rw [← lintegral_finset, Finset.coe_univ, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
inst_2 : Fintype α
f : α → ℝ≥0∞
rw : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in (↑Finset.univ : Set α), f x ∂μ
⊢ ∫⁻ (x : α), f x ∂μ = ∑ x : α, HMul.hMul (β := ℝ≥0∞) (f x) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
have rw₁ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in univ, f x ∂μ
Tactic: rw [← lintegral_finset, Finset.coe_univ, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : MeasurableSingletonClass α
inst_2 : Fintype α
f : α → ℝ≥0∞
rw : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in (↑Finset.univ : Set α), f x ∂μ
rw₁ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α) in univ, f x ∂μ
⊢ ∫⁻ (x : α), f x ∂μ = ∑ x : α, HMul.hMul (β := ℝ≥0∞) (f x) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞)
have rw₂ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
Tactic: rw [← lintegral_finset, Finset.coe_univ, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
have rsuffices : ∀ (g : α → ℝ≥0∞) (hgm : Measurable g) (hgle : g ≤ f)
  (hleg : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ),
  ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
Tactic: rsuffices ⟨g, hgm, hgle, hleg⟩ :
      ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ ∀ s, ∫⁻ a in s, f a ∂μ ≤ ∫⁻ a in s, g a ∂μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f : α → ℝ≥0∞
rsuffices :
  ∀ (g : α → ℝ≥0∞) (hgm : Measurable g) (hgle : g ≤ f)
    (hleg : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
have rsuffices₁ : ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Tactic: rsuffices ⟨g, hgm, hgle, hleg⟩ :
      ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ ∀ s, ∫⁻ a in s, f a ∂μ ≤ ∫⁻ a in s, g a ∂μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have inr : ∀
  (this :
    ∀ (μ : Measure α) [SFinite μ] (h : IsFiniteMeasure μ),
      ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ)
  (h : ¬IsFiniteMeasure μ),
  ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Tactic: wlog h : IsFiniteMeasure μ generalizing μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f : α → ℝ≥0∞
inr :
  ∀
    (this :
      ∀ (μ : Measure α) [SFinite μ] (h : IsFiniteMeasure μ),
        ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ)
    (h : ¬IsFiniteMeasure μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have wlog : ∀ (μ : Measure α) [SFinite μ] (h : IsFiniteMeasure μ),
  ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Tactic: wlog h : IsFiniteMeasure μ generalizing μ
Cleared hypotheses: inst_1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [SFinite μ] (h : IsFiniteMeasure μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have inr : ∀ (g : (n : ℕ) → α → ℝ≥0∞) (hgm : ∀ (n : ℕ), Measurable (g n)) (hgle : ∀ (n : ℕ), g n ≤ f)
  (hgint : ∀ (n : ℕ) (s : Set α), ∫⁻ (a : α) in s, f a ∂sfiniteSeq μ n ≤ ∫⁻ (a : α) in s, g n a ∂sfiniteSeq μ n),
  ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Tactic: choose g hgm hgle hgint using fun n ↦ @this (sfiniteSeq μ n) _ inferInstance
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [SFinite μ] (h : IsFiniteMeasure μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgle : ∀ (n : ℕ), g n ≤ f
hgint : ∀ (n : ℕ) (s : Set α), ∫⁻ (a : α) in s, f a ∂sfiniteSeq μ n ≤ ∫⁻ (a : α) in s, g n a ∂sfiniteSeq μ n
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have inr : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ
Tactic: refine ⟨fun x ↦ ⨆ n, g n x, .iSup hgm, fun x ↦ iSup_le (hgle · x), fun s ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [SFinite μ] (h : IsFiniteMeasure μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgle : ∀ (n : ℕ), g n ≤ f
hgint : ∀ (n : ℕ) (s : Set α), ∫⁻ (a : α) in s, f a ∂sfiniteSeq μ n ≤ ∫⁻ (a : α) in s, g n a ∂sfiniteSeq μ n
s : Set α
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ
have inr : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (a : α) in s, f a ∂sfiniteSeq μ i)
  (∑' (i : ℕ), ∫⁻ (a : α) in s, ⨆ (n : ℕ), g n a ∂sfiniteSeq μ i)
Tactic: rw [← sum_sfiniteSeq μ, Measure.restrict_sum_of_countable,
      lintegral_sum_measure, lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have this : ∀ (n : ℕ),
  ∃ (g : α → ℝ≥0∞),
    Measurable g ∧ g ≤ f ∧ g ≤ (↑n : α → ℝ≥0∞) ∧ ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g a ∂μ
Tactic: have (n : ℕ) : ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ g ≤ n ∧
      ∫⁻ a, min (f a) n ∂μ = ∫⁻ a, g a ∂μ := by
    simpa [and_assoc] using exists_measurable_le_lintegral_eq μ (f ⊓ n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
this :
  ∀ (n : ℕ),
    ∃ (g : α → ℝ≥0∞),
      Measurable g ∧ g ≤ f ∧ g ≤ (↑n : α → ℝ≥0∞) ∧ ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have choose : ∀ (g : (n : ℕ) → α → ℝ≥0∞) (hgm : ∀ (n : ℕ), Measurable (g n)) (hgf : ∀ (n : ℕ), g n ≤ f)
  (hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞))
  (hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ),
  ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Tactic: choose g hgm hgf hgle hgint using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have hφm : Measurable φ
Tactic: have hφm : Measurable φ := by fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have hφle : φ ≤ f
Tactic: have hφle : φ ≤ f := fun x ↦ iSup_le (hgf · x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have refine : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, φ a ∂μ
Tactic: refine ⟨φ, hφm, hφle, fun s ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, φ a ∂μ
have rw : ⨆ (φ : SimpleFunc α ℝ≥0),
    ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) ≤
  ∫⁻ (a : α) in s, φ a ∂μ
Tactic: rw [lintegral_eq_nnreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
⊢ ⨆ (φ : SimpleFunc α ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) ≤
    ∫⁻ (a : α) in s, φ a ∂μ
have refine : ∀ (ψ : SimpleFunc α ℝ≥0) (hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
  (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ
Tactic: refine iSup₂_le fun ψ hψ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ ∃ (n : ℕ), ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)
have rcases : ∀ (C : ℝ≥0) (hC : C ∈ upperBounds (↑ψ.range : Set ℝ≥0)),
  ∃ (n : ℕ), ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)
Tactic: rcases ψ.range.bddAbove with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ
have obtain : ∀ (n : ℕ) (hn : ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)),
  (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ
Tactic: obtain ⟨n, hn⟩ : ∃ n : ℕ, ∀ x, ψ x ≤ n := by
    rcases ψ.range.bddAbove with ⟨C, hC⟩
    exact ⟨⌈C⌉₊, fun x ↦ (hC <| ψ.mem_range_self x).trans (Nat.le_ceil _)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
n : ℕ
hn : ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)
⊢ ∫⁻ (a : α) in s, min (f a) (↑n : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ
have this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ ≠ ∞
Tactic: have : ∫⁻ a in (toMeasurable μ s)ᶜ, min (f a) n ∂μ ≠ ∞ :=
        IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal _ ⟨n, fun _ ↦ min_le_right ..⟩ |>.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
n : ℕ
hn : ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ ≠ ∞
⊢ ∫⁻ (a : α) in s, min (f a) (↑n : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ
have hsm : MeasurableSet (toMeasurable μ s)
Tactic: have hsm : MeasurableSet (toMeasurable μ s) := measurableSet_toMeasurable ..
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
n : ℕ
hn : ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ ≠ ∞
hsm : MeasurableSet (toMeasurable μ s)
⊢ ∫⁻ (a : α) in s, min (f a) (↑n : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ
have apply : ∫⁻ (a : α) in s, min (f a) (↑n : ℝ≥0∞) ∂μ + ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ ≤
  ∫⁻ (a : α) in s, g n a ∂μ + ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ
Tactic: apply ENNReal.le_of_add_le_add_right this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
n : ℕ
hn : ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ ≠ ∞
hsm : MeasurableSet (toMeasurable μ s)
⊢ ∫⁻ (a : α) in s, min (f a) (↑n : ℝ≥0∞) ∂μ + ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ ≤
    ∫⁻ (a : α) in s, g n a ∂μ + ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ
have rw : ∫⁻ (x : α) in toMeasurable μ s, g n x ∂μ + ∫⁻ (x : α) in (toMeasurable μ s)ᶜ, g n x ∂μ ≤
  ∫⁻ (a : α) in toMeasurable μ s, g n a ∂μ + ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ
Tactic: rw [← μ.restrict_toMeasurable_of_sFinite, lintegral_add_compl _ hsm, hgint,
        ← lintegral_add_compl _ hsm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Countable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ (↑n : α → ℝ≥0∞)
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun (x : α) ↦ ⨆ (n : ℕ), g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x
n : ℕ
hn : ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ ≠ ∞
hsm : MeasurableSet (toMeasurable μ s)
⊢ ∫⁻ (x : α) in toMeasurable μ s, g n x ∂μ + ∫⁻ (x : α) in (toMeasurable μ s)ᶜ, g n x ∂μ ≤
    ∫⁻ (a : α) in toMeasurable μ s, g n a ∂μ + ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) (↑n : ℝ≥0∞) ∂μ
have bc : ∀ (x : α), g n x ≤ min (f x) (↑n : ℝ≥0∞)
Tactic: gcongr with x