case inl
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
h₀ : (∫⁻ (a : α), f a ∂μ) = 0
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ

case inr
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
h₀ : (∫⁻ (a : α), f a ∂μ) ≠ 0
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ
cases' eq_or_ne (∫⁻ a, f a ∂μ) 0 with h₀ h₀
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ
case inr
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
h₀ : (∫⁻ (a : α), f a ∂μ) ≠ 0
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ
rcases exists_seq_strictMono_tendsto' h₀.bot_lt with ⟨L, _, hLf, hL_tendsto⟩
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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, Measurable g ∧ g ≤ f ∧ L n < ∫⁻ (a : α), g a ∂μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ
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
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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, Measurable g ∧ g ≤ f ∧ L n < ∫⁻ (a : α), g a ∂μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ
choose g hgm hgf hLg using this
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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∞
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) a ∂μ

case inr.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
⊢ (∫⁻ (a : α), (fun x => ⨆ (n : ℕ), g n x) a ∂μ) ≤ ∫⁻ (a : α), f a ∂μ
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ
refine'
  ⟨fun x => ⨆ n, g n x, measurable_iSup hgm, fun x => iSup_le fun n => hgf n x, le_antisymm _ _⟩
no goals
case inl
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
h₀ : (∫⁻ (a : α), f a ∂μ) = 0
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), g a ∂μ
exact ⟨0, measurable_zero, zero_le f, h₀.trans lintegral_zero.symm⟩
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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 ∂μ))
n : ℕ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ L n < ∫⁻ (a : α), g a ∂μ
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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 ∂μ))
⊢ ∀ (n : ℕ), ∃ g, Measurable g ∧ g ≤ f ∧ L n < ∫⁻ (a : α), g a ∂μ
intro n
no goals
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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 ∂μ))
n : ℕ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ L n < ∫⁻ (a : α), g a ∂μ
simpa only [← iSup_lintegral_measurable_le_eq_lintegral f, lt_iSup_iff, exists_prop] using
  (hLf n).2
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
n : ℕ
x : α
⊢ g n x ≤ (fun x => ⨆ (n : ℕ), g n x) x
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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∞
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) a ∂μ
refine' le_of_tendsto' hL_tendsto fun n => (hLg n).le.trans <| lintegral_mono fun x => _
no goals
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
n : ℕ
x : α
⊢ g n x ≤ (fun x => ⨆ (n : ℕ), g n x) x
exact le_iSup (fun n => g n x) n
no goals
case inr.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.77053
γ : Type ?u.77056
δ : Type ?u.77059
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∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
⊢ (∫⁻ (a : α), (fun x => ⨆ (n : ℕ), g n x) a ∂μ) ≤ ∫⁻ (a : α), f a ∂μ
exact lintegral_mono fun x => iSup_le fun n => hgf n x