-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem tendsto_lintegral_filter_of_dominated_convergence {ι} {l : Filter ι}
    [l.IsCountablyGenerated] {F : ι → α → ℝ≥0∞} {f : α → ℝ≥0∞} (bound : α → ℝ≥0∞)
    (hF_meas : ∀ᶠ n in l, Measurable (F n)) (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, F n a ≤ bound a)
    (h_fin : ∫⁻ a, bound a ∂μ ≠ ∞) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))) :
    Tendsto (fun n => ∫⁻ a, F n a ∂μ) l (𝓝 <| ∫⁻ a, f a ∂μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h : ∃ a, ∀ b ≥ a, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
rcases h with ⟨k, h⟩

Result:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Proof state:
case intro.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ n✝ + k ≥ k

Tactic:
exact Nat.le_add_left _ _

Result:
no goals

Proof state:
case intro.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ ∀ (n : ℕ), F (x (n + k)) ≤ᶠ[ae μ] bound

Tactic:
intro

Result:
case intro.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ F (x (n✝ + k)) ≤ᶠ[ae μ] bound

Proof state:
case intro.refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ ∫⁻ (a : α), bound a ∂μ ≠ ⊤

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl✝ : Tendsto x atTop l
xl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
⊢ ?m.350341

Tactic:
exact xl

Result:
no goals

Proof state:
case intro.refine_5.hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto x atTop l

Tactic:
assumption

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ ∀ (n : ℕ), Measurable (F (x (n + k)))

Tactic:
intro

Result:
case intro.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ Measurable (F (x (n✝ + k)))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ ?m.350341

Tactic:
rw [tendsto_atTop'] at xl

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl✝ : Tendsto x atTop l
xl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
⊢ ?m.350341