α : Type u_1
ι : Type ?u.93118
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
α : Type u_1
ι : Type ?u.93118
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
⊢ Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
have lim₁ := lintegral_tendsto_of_monotone_of_nat hφ.biInter_Ici_aecover
  (fun i j hij => biInter_subset_biInter_left (Ici_subset_Ici.mpr hij)) hfm
α : Type u_1
ι : Type ?u.93118
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
α : Type u_1
ι : Type ?u.93118
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
have lim₂ := lintegral_tendsto_of_monotone_of_nat hφ.biUnion_Iic_aecover
  (fun i j hij => biUnion_subset_biUnion_left (Iic_subset_Iic.mpr hij)) hfm
case refine_1
α : Type u_1
ι : Type ?u.93118
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
n : ℕ
⊢ (∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici n), φ k, f x ∂μ) ≤ ∫⁻ (x : α) in φ n, f x ∂μ

case refine_2
α : Type u_1
ι : Type ?u.93118
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
n : ℕ
⊢ (∫⁻ (x : α) in φ n, f x ∂μ) ≤ ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic n), φ k, f x ∂μ
α : Type u_1
ι : Type ?u.93118
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
refine tendsto_of_tendsto_of_tendsto_of_le_of_le lim₁ lim₂ (fun n ↦ ?_) fun n ↦ ?_
no goals
case refine_1
α : Type u_1
ι : Type ?u.93118
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
n : ℕ
⊢ (∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici n), φ k, f x ∂μ) ≤ ∫⁻ (x : α) in φ n, f x ∂μ

case refine_2
α : Type u_1
ι : Type ?u.93118
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
φ : ℕ → Set α
hφ : AECover μ atTop φ
f : α → ℝ≥0∞
hfm : AEMeasurable f
lim₁ : Tendsto (fun i => ∫⁻ (x : α) in ⋂ (k : ℕ) (_ : k ∈ Ici i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
lim₂ : Tendsto (fun i => ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic i), φ k, f x ∂μ) atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
n : ℕ
⊢ (∫⁻ (x : α) in φ n, f x ∂μ) ≤ ∫⁻ (x : α) in ⋃ (k : ℕ) (_ : k ∈ Iic n), φ k, f x ∂μ
exacts [lintegral_mono_set (biInter_subset_of_mem left_mem_Ici),
  lintegral_mono_set (subset_biUnion_of_mem right_mem_Iic)]