∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α) {s t : Set α} {Ixx : α → α → Set α}
  [Filter.TendstoIxxClass Ixx (nhds a) (nhds a)] [Filter.TendstoIxxClass Ixx (Filter.principal s) (Filter.principal t)],
  Filter.TendstoIxxClass Ixx (nhdsWithin a s) (nhdsWithin a t)