-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem tendsto_setToFun_filter_of_dominated_convergence (hT : DominatedFinMeasAdditive μ T C) {ι}
    {l : Filter ι} [l.IsCountablyGenerated] {fs : ι → α → E} {f : α → E} (bound : α → ℝ)
    (hfs_meas : ∀ᶠ n in l, AEStronglyMeasurable (fs n) μ)
    (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, ‖fs n a‖ ≤ bound a) (bound_integrable : Integrable bound μ)
    (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))) :
    Tendsto (fun n => setToFun μ T hT (fs n)) l (𝓝 <| setToFun μ T hT f)

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ Tendsto ((fun n => setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))

Tactic:
have hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s := by rwa [tendsto_atTop'] at xl

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
⊢ Tendsto ((fun n => setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))

Proof state:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h✝ : {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l
k : ℕ
h :
  ∀ b ≥ k, x b ∈ {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}
a : α
h_lin : Tendsto (fun n => fs n a) l (𝓝 (f a))
⊢ Tendsto (fun n => x (n + k)) atTop l

Tactic:
rw [tendsto_add_atTop_iff_nat]

Result:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h✝ : {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l
k : ℕ
h :
  ∀ b ≥ k, x b ∈ {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}
a : α
h_lin : Tendsto (fun n => fs n a) l (𝓝 (f a))
⊢ Tendsto x atTop l

Proof state:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h✝ : {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l
k : ℕ
h :
  ∀ b ≥ k, x b ∈ {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}
⊢ ∀ (a : α), Tendsto (fun n => fs n a) l (𝓝 (f a)) → Tendsto (fun n => fs (x (n + k)) a) atTop (𝓝 (f a))

Tactic:
refine fun a h_lin => @Tendsto.comp _ _ _ (fun n => x (n + k)) (fun n => fs n a) _ _ _ h_lin ?_

Result:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h✝ : {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l
k : ℕ
h :
  ∀ b ≥ k, x b ∈ {x | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}
a : α
h_lin : Tendsto (fun n => fs n a) l (𝓝 (f a))
⊢ Tendsto (fun n => x (n + k)) atTop l