∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [inst : UniformSpace β] {F : ι → UniformFun α β}
  {f : UniformFun α β}, Filter.Tendsto F p (nhds f) ↔ TendstoUniformly (⇑UniformFun.toFun ∘ F) (UniformFun.toFun f) p