-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem exists_measurable_le_forall_setLIntegral_eq [SFinite μ] (f : α → ℝ≥0∞) :
    ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ ∀ s, ∫⁻ a in s, f a ∂μ = ∫⁻ a in s, g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, 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)

Result:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
this : ∀ (n : ℕ), ∃ g, Measurable g ∧ g ≤ f ∧ g ≤ ↑n ∧ ∫⁻ (a : α), f a ⊓ ↑n ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), f a ⊓ ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x => ⨆ n, g n x
⊢ Measurable φ

Tactic:
measurability

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Tactic:
wlog h : IsFiniteMeasure μ generalizing μ

Result:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [inst : SFinite μ],
    IsFiniteMeasure μ → ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), f a ⊓ ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x => ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
⊢ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ

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

Result:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), f a ⊓ ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x => ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ∫⁻ (a : α) in s, φ a ∂μ

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [inst : SFinite μ],
    IsFiniteMeasure μ → ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
g : ℕ → α → ℝ≥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) a ∂μ

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

Result:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [inst : SFinite μ],
    IsFiniteMeasure μ → ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
g : ℕ → α → ℝ≥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 α
⊢ ∑' (i : ℕ), ∫⁻ (a : α) in s, f a ∂sfiniteSeq μ i ≤ ∑' (i : ℕ), ∫⁻ (a : α) in s, ⨆ n, g n a ∂sfiniteSeq μ i

Proof state:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), f a ⊓ ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x => ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, f a ⊓ ↑n ∂μ ≠ ⊤
⊢ ∫⁻ (a : α) in s, f a ⊓ ↑n ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ

Tactic:
have hsm : MeasurableSet (toMeasurable μ s) := measurableSet_toMeasurable ..

Result:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), f a ⊓ ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x => ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, f a ⊓ ↑n ∂μ ≠ ⊤
hsm : MeasurableSet (toMeasurable μ s)
⊢ ∫⁻ (a : α) in s, f a ⊓ ↑n ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ

Proof state:
case bc.hfg
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), f a ⊓ ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x => ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, f a ⊓ ↑n ∂μ ≠ ⊤
hsm : MeasurableSet (toMeasurable μ s)
x : α
⊢ g n x ≤ f x ⊓ ↑n

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

Result:
no goals

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [inst : SFinite μ],
    IsFiniteMeasure μ → ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
⊢ ∃ g, 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

Result:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
this :
  ∀ (μ : Measure α) [inst : SFinite μ],
    IsFiniteMeasure μ → ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
h : ¬IsFiniteMeasure μ
g : ℕ → α → ℝ≥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, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ