awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 ∂μ

Tactic:
⟨fun x ↦ ⨆ n, g n x, .iSup hgm, fun x ↦ iSup_le (hgle · x), fun s ↦ ?_⟩

Premises used: iSup, Measurable.iSup, And.intro, Exists.intro, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
inr : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
refine ⟨fun x ↦ ⨆ n, g n x, .iSup hgm, fun x ↦ iSup_le (hgle · x), fun s ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 α
inr :
  LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (a : α) in s, f a ∂sfiniteSeq μ i)
    (∑' (i : ℕ), ∫⁻ (a : α) in s, ⨆ (n : ℕ), g n a ∂sfiniteSeq μ i)
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ

Tactic:
rw [← sum_sfiniteSeq μ, Measure.restrict_sum_of_countable,
      lintegral_sum_measure, lintegral_sum_measure]

Premises used: MeasureTheory.Measure.restrict_sum_of_countable, MeasureTheory.sum_sfiniteSeq, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 α
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (a : α) in s, f a ∂sfiniteSeq μ i)
    (∑' (i : ℕ), ∫⁻ (a : α) in s, ⨆ (n : ℕ), g n a ∂sfiniteSeq μ i)

Tactic:
ENNReal.tsum_le_tsum fun n ↦ (hgint n s).trans (lintegral_mono fun x ↦ le_iSup (g · x) _)

Premises used: ENNReal.tsum_le_tsum, le_iSup, MeasureTheory.lintegral_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 α
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (a : α) in s, f a ∂sfiniteSeq μ i)
    (∑' (i : ℕ), ∫⁻ (a : α) in s, ⨆ (n : ℕ), g n a ∂sfiniteSeq μ i)

Tactic:
exact ENNReal.tsum_le_tsum fun n ↦ (hgint n s).trans (lintegral_mono fun x ↦ le_iSup (g · x) _)

Premises used: ENNReal.tsum_le_tsum, le_iSup, MeasureTheory.lintegral_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
n : ℕ
⊢ ∃ (g : α → ℝ≥0∞),
    Measurable g ∧ g ≤ f ∧ g ≤ (↑n : α → ℝ≥0∞) ∧ ∫⁻ (a : α), min (f a) (↑n : ℝ≥0∞) ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
simpa [and_assoc] using exists_measurable_le_lintegral_eq μ (f ⊓ n)

Premises used: Nat.cast, and_assoc, MeasureTheory.exists_measurable_le_lintegral_eq, Min.min
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
Goal:
α : Type u_1
inst : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst_1 : SFinite μ
h : IsFiniteMeasure μ
⊢ ∀ (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)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 ∂μ
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 ∂μ
⊢ ∃ (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
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
⊢ Measurable φ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
⊢ Measurable φ

Tactic:
have hφm : Measurable φ := by fun_prop
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 φ
⊢ φ ≤ f

Tactic:
have hφle : φ ≤ f := fun x ↦ iSup_le (hgf · x)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 ∂μ

Tactic:
⟨φ, hφm, hφle, fun s ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
refine : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, φ a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
refine ⟨φ, hφm, hφle, fun s ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 α
rw :
  ⨆ (φ : SimpleFunc α ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) ≤
    ∫⁻ (a : α) in s, φ a ∂μ
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, φ a ∂μ

Tactic:
rw [lintegral_eq_nnreal]

Premises used: MeasureTheory.lintegral_eq_nnreal
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 ∂μ

Tactic:
iSup₂_le fun ψ hψ ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 α
refine :
  ∀ (ψ : SimpleFunc α ℝ≥0) (hψ : ∀ (x : α), (↑((ψ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x),
    (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ
⊢ ⨆ (φ : SimpleFunc α ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) ≤
    ∫⁻ (a : α) in s, φ a ∂μ

Tactic:
refine iSup₂_le fun ψ hψ ↦ ?_

Premises used: iSup₂_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
rcases :
  ∀ (C : ℝ≥0) (hC : C ∈ upperBounds (↑ψ.range : Set ℝ≥0)),
    ∃ (n : ℕ), ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)
⊢ ∃ (n : ℕ), ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)

Tactic:
rcases ψ.range.bddAbove with ⟨C, hC⟩

Premises used: Finset.bddAbove, MeasureTheory.SimpleFunc.range
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
C : ℝ≥0
hC : C ∈ upperBounds (↑ψ.range : Set ℝ≥0)
⊢ ∃ (n : ℕ), ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)

Tactic:
⟨⌈C⌉₊, fun x ↦ (hC <| ψ.mem_range_self x).trans (Nat.le_ceil _)⟩

Premises used: Nat.ceil, Exists.intro, Nat.le_ceil, LE.le.trans, MeasureTheory.SimpleFunc.mem_range_self
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
C : ℝ≥0
hC : C ∈ upperBounds (↑ψ.range : Set ℝ≥0)
⊢ ∃ (n : ℕ), ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)

Tactic:
exact ⟨⌈C⌉₊, fun x ↦ (hC <| ψ.mem_range_self x).trans (Nat.le_ceil _)⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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
obtain :
  ∀ (n : ℕ) (hn : ∀ (x : α), LE.le (α := ℝ≥0) ((ψ : (a : α) → ℝ≥0) x : ℝ≥0) ((↑n : ℝ≥0) : ℝ≥0)),
    (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ
⊢ (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 _)⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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)
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) = ∫⁻ (a : α) in s, (↑((ψ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ

Tactic:
SimpleFunc.lintegral_eq_lintegral .. |>.symm

Premises used: ENNReal.ofNNReal, WithTop.some, Eq.symm, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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, (↑((ψ : (a : α) → ℝ≥0) a) : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α) in s, min (f a) (↑n : ℝ≥0∞) ∂μ

Tactic:
lintegral_mono fun a ↦ le_min (hψ _) (ENNReal.coe_le_coe.2 (hn a))

Premises used: Iff.mpr, ENNReal.coe_le_coe, le_min, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 (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
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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∞) ∂μ ≠ ∞
⊢ MeasurableSet (toMeasurable μ s)

Tactic:
have hsm : MeasurableSet (toMeasurable μ s) := measurableSet_toMeasurable ..
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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)
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∞) ∂μ
⊢ ∫⁻ (a : α) in s, min (f a) (↑n : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ

Tactic:
apply ENNReal.le_of_add_le_add_right this

Premises used: ENNReal.le_of_add_le_add_right
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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)
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∞) ∂μ
⊢ ∫⁻ (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:
rw [← μ.restrict_toMeasurable_of_sFinite, lintegral_add_compl _ hsm, hgint,
        ← lintegral_add_compl _ hsm]

Premises used: MeasureTheory.lintegral_add_compl, MeasureTheory.Measure.restrict_toMeasurable_of_sFinite
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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)
bc : ∀ (x : α), g n x ≤ min (f x) (↑n : ℝ≥0∞)
⊢ ∫⁻ (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:
gcongr with x
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 : α
⊢ g n x ≤ min (f x) (↑n : ℝ≥0∞)

Tactic:
le_min (hgf n x) (hgle n x)

Premises used: le_min
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable
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 : α
⊢ g n x ≤ min (f x) (↑n : ℝ≥0∞)

Tactic:
exact le_min (hgf n x) (hgle n x)

Premises used: le_min