α : Type u_2
ι : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ (⨆ (i : ι), ∫⁻ (x : α) in φ i, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
α : Type u_2
ι : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
⊢ (⨆ (i : ι), ∫⁻ (x : α) in φ i, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
have := hφ.lintegral_tendsto_of_countably_generated hfm
α : Type u_2
ι : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
α : Type u_2
ι : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ (⨆ (i : ι), ∫⁻ (x : α) in φ i, f x ∂μ) = ∫⁻ (x : α), f x ∂μ
refine' ciSup_eq_of_forall_le_of_forall_lt_exists_gt
  (fun i => lintegral_mono' Measure.restrict_le_self le_rfl) fun w hw => _
case intro.intro
α : Type u_2
ι : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
m : ℝ≥0∞
hm₁ : w < m
hm₂ : m < ∫⁻ (x : α), f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
α : Type u_2
ι : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
rcases exists_between hw with ⟨m, hm₁, hm₂⟩
case intro.intro.intro
α : Type u_2
ι : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
m : ℝ≥0∞
hm₁ : w < m
hm₂ : m < ∫⁻ (x : α), f x ∂μ
i : ι
hi : m ≤ ∫⁻ (x : α) in φ i, f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
case intro.intro
α : Type u_2
ι : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
m : ℝ≥0∞
hm₁ : w < m
hm₂ : m < ∫⁻ (x : α), f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
rcases(eventually_ge_of_tendsto_gt hm₂ this).exists with ⟨i, hi⟩
no goals
case intro.intro.intro
α : Type u_2
ι : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
m : ℝ≥0∞
hm₁ : w < m
hm₂ : m < ∫⁻ (x : α), f x ∂μ
i : ι
hi : m ≤ ∫⁻ (x : α) in φ i, f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
exact ⟨i, lt_of_lt_of_le hm₁ hi⟩