no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
ha : s ⊆ Ioi a
hs : Set.Nonempty s → ∃ b, b > a ∧ Ioo a b ⊆ s
h : Set.Nonempty (↑ofDual ⁻¹' s)
⊢ ∃ a_1, a_1 < ↑toDual a ∧ Ioo a_1 (↑toDual a) ⊆ ↑ofDual ⁻¹' s
simpa only [OrderDual.exists, dual_Ioo] using hs h