∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [inst : UniformSpace β] {𝔖 : Set (Set α)}
  {F : ι → UniformOnFun α β 𝔖} {f : UniformOnFun α β 𝔖},
  Filter.Tendsto F p (nhds f) = ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ F) ((UniformOnFun.toFun 𝔖) f) p s