no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
a✝ b✝ : α
inst✝ : TopologicalSpace γ
a b c : α
H : b ∈ Ioc a c
⊢ Ioo a c ∈ 𝓝[Iio b] b
simpa only [dual_Ioo] using
  Ioo_mem_nhdsWithin_Ioi (show toDual b ∈ Ico (toDual c) (toDual a) from H.symm)