∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [inst_3 : LocallyFiniteOrder R]
  [Archimedean R] [Nontrivial R], Filter.Tendsto (fun n => Finset.Ioo (-↑n) ↑n) Filter.atTop Filter.atTop