no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p'✝ : Filter α
g✝ : ι → α
g : ι → β
b : β
hg : Tendsto g p (𝓝 b)
p' : Filter α
⊢ TendstoUniformlyOnFilter (fun n x => g n) (fun x => b) p p'
simpa only [nhds_eq_comap_uniformity, tendsto_comap_iff] using hg.comp (tendsto_fst (g := p'))