case refine_1
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝¹ : IsCountablyGenerated L
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (f ω))
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : Ω) ∂μ, ↑(↑(fs n) a) ≤ (fun x => ↑c) a

case refine_2
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝¹ : IsCountablyGenerated L
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (f ω))
⊢ ∀ᵐ (a : Ω) ∂μ, Tendsto (fun n => ↑(↑(fs n) a)) L (𝓝 ↑(f a))
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝¹ : IsCountablyGenerated L
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (f ω))
⊢ Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑(fs i) ω) ∂μ) L (𝓝 (∫⁻ (ω : Ω), ↑(f ω) ∂μ))
refine tendsto_lintegral_filter_of_dominated_convergence (fun _ => c)
  (eventually_of_forall fun i => (ENNReal.continuous_coe.comp (fs i).continuous).measurable) ?_
  (@lintegral_const_lt_top _ _ μ _ _ (@ENNReal.coe_ne_top c)).ne ?_
no goals
case refine_1
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝¹ : IsCountablyGenerated L
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (f ω))
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : Ω) ∂μ, ↑(↑(fs n) a) ≤ (fun x => ↑c) a
simpa only [Function.comp_apply, ENNReal.coe_le_coe] using fs_le_const
no goals
case refine_2
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝¹ : IsCountablyGenerated L
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, ↑(fs i) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (f ω))
⊢ ∀ᵐ (a : Ω) ∂μ, Tendsto (fun n => ↑(↑(fs n) a)) L (𝓝 ↑(f a))
simpa only [Function.comp_apply, ENNReal.tendsto_coe] using fs_lim