-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem tendsto_lintegral_of_dominated_convergence' {F : ℕ → α → ℝ≥0∞} {f : α → ℝ≥0∞}
    (bound : α → ℝ≥0∞) (hF_meas : ∀ n, AEMeasurable (F n) μ) (h_bound : ∀ n, F n ≤ᵐ[μ] bound)
    (h_fin : ∫⁻ a, bound a ∂μ ≠ ∞) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))) :
    Tendsto (fun n => ∫⁻ a, F n a ∂μ) atTop (𝓝 (∫⁻ a, f a ∂μ))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))

Tactic:
have : ∀ n, ∀ᵐ a ∂μ, (hF_meas n).mk (F n) a = F n a := fun n => (hF_meas n).ae_eq_mk.symm

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
this✝ : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
this : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
this✝¹ : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
this✝ : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
this : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
a : α
H : ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
H' : Tendsto (fun n => F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun n => F n a) atTop (𝓝 (f a))

Tactic:
exact H'

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ Tendsto (fun n => ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
apply
  tendsto_lintegral_of_dominated_convergence bound (fun n => (hF_meas n).measurable_mk) _ h_fin

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))

α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ ≤ᶠ[ae μ] bound

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ ≤ᶠ[ae μ] bound

Tactic:
intro n

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
n : ℕ
⊢ AEMeasurable.mk (F n) ⋯ ≤ᶠ[ae μ] bound