-- 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 ∂μ
this : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))

Tactic:
have : ∀ᵐ a ∂μ, ∀ n, (hF_meas n).mk (F n) a = F n a := ae_all_iff.mpr this

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
this : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (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 ∂μ
n : ℕ
⊢ AEMeasurable.mk (F n) ⋯ ≤ᶠ[ae μ] bound

Tactic:
filter_upwards [h_bound n, (hF_meas n).ae_eq_mk] with a H H'

Result:
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 ∂μ
n : ℕ
a : α
H : F n a ≤ bound a
H' : F n a = AEMeasurable.mk (F n) ⋯ a
⊢ AEMeasurable.mk (F n) ⋯ a ≤ bound 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 ∂μ
n : ℕ
a : α
H : F n a ≤ bound a
H' : F n a = AEMeasurable.mk (F n) ⋯ a
⊢ AEMeasurable.mk (F n) ⋯ a ≤ bound a

Tactic:
rwa [H'] at 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))
⊢ Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
have : ∀ n, ∫⁻ a, F n a ∂μ = ∫⁻ a, (hF_meas n).mk (F n) a ∂μ := fun n =>
  lintegral_congr_ae (hF_meas n).ae_eq_mk

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 ∂μ
⊢ 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 ∂μ
this✝ : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
this : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))

Tactic:
filter_upwards [this, h_lim] with a H H'

Result:
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 => AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (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 ∂μ
⊢ Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
simp_rw [this]

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 ∂μ
⊢ Tendsto (fun n => ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ) atTop (𝓝 (∫⁻ (a : α), 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 => AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))

Tactic:
simp_rw [H]

Result:
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))