-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem map_coe_atTop_of_Ioo_subset (hb : s ⊆ Iio b) (hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s) :
    map ((↑) : s → α) atTop = 𝓝[<] b

Proof state:
case inr.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ map Subtype.val atTop = 𝓝[<] b

Tactic:
rw [← comap_coe_nhdsLT_of_Ioo_subset hb fun _ => hs a ha, map_comap_of_mem]

Result:
case inr.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ range Subtype.val ∈ 𝓝[<] b

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
⊢ map Subtype.val atTop = 𝓝[<] b

Tactic:
rcases eq_empty_or_nonempty (Iio b) with (hb' | ⟨a, ha⟩)

Result:
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb' : Iio b = ∅
⊢ map Subtype.val atTop = 𝓝[<] b

case inr.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ map Subtype.val atTop = 𝓝[<] b

Proof state:
case inr.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ range Subtype.val ∈ 𝓝[<] b

Tactic:
rw [Subtype.range_val]

Result:
case inr.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ s ∈ 𝓝[<] b

Proof state:
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb' : Iio b = ∅
this : IsEmpty ↑s
⊢ map Subtype.val atTop = 𝓝[<] b

Tactic:
rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb' : Iio b = ∅
⊢ map Subtype.val atTop = 𝓝[<] b

Tactic:
have : IsEmpty s := ⟨fun x => hb'.subset (hb x.2)⟩

Result:
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb' : Iio b = ∅
this : IsEmpty ↑s
⊢ map Subtype.val atTop = 𝓝[<] b

Proof state:
case inr.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
a : α
ha : a ∈ Iio b
⊢ s ∈ 𝓝[<] b

Tactic:
exact (mem_nhdsLT_iff_exists_Ioo_subset' ha).2 (hs a ha)

Result:
no goals