α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
ha : s ⊆ Ioi a
hs : ∀ (b' : α), b' > a → ∃ b, b > a ∧ Ioo a b ⊆ s
b' : αᵒᵈ
hb' : b' < ↑toDual a
⊢ ∃ a_1, a_1 < ↑toDual a ∧ Ioo a_1 (↑toDual a) ⊆ ↑ofDual ⁻¹' s
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
ha : s ⊆ Ioi a
hs : ∀ (b' : α), b' > a → ∃ b, b > a ∧ Ioo a b ⊆ s
⊢ map Subtype.val atBot = 𝓝[Ioi a] a
refine' (map_coe_atTop_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from ha)
  fun b' hb' => _ : _)
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 : ∀ (b' : α), b' > a → ∃ b, b > a ∧ Ioo a b ⊆ s
b' : αᵒᵈ
hb' : b' < ↑toDual a
⊢ ∃ a_1, a_1 < ↑toDual a ∧ Ioo a_1 (↑toDual a) ⊆ ↑ofDual ⁻¹' s
simpa only [OrderDual.exists, dual_Ioo] using hs b' hb'