∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a : X} {α : Type u_2}
  {l : Filter α} {f : α → ↑(Set.Ioi a)},
  autoParam (Order.IsPredPrelimit a) tendsto_Ioi_atBot._auto_1 →
    Filter.Tendsto f l Filter.atBot = Filter.Tendsto (fun x => ↑(f x)) l (nhdsWithin a (Set.Ioi a))