∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {s : Set X} {b : X},
  s ⊆ Set.Iio b →
    (∀ a' < b, ∃ a < b, Set.Ioo a b ⊆ s) →
      autoParam (Order.IsSuccPrelimit b) map_coe_atTop_of_Ioo_subset._auto_1 →
        Filter.map Subtype.val Filter.atTop = nhdsWithin b (Set.Iio b)