no goals
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
h : a < b
s : Set α
⊢ TFAE
    [s ∈ 𝓝[Iic b] b, s ∈ 𝓝[Icc a b] b, s ∈ 𝓝[Ioc a b] b, ∃ l, l ∈ Ico a b ∧ Ioc l b ⊆ s, ∃ l, l ∈ Iio b ∧ Ioc l b ⊆ s]
simpa only [exists_prop, OrderDual.exists, dual_Ici, dual_Ioc, dual_Icc, dual_Ico] using
  TFAE_mem_nhdsWithin_Ici h.dual (ofDual ⁻¹' s)