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

Proof state:
case intro.intro.h.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
a✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[<] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
⊢ u ∈ atTop

Tactic:
obtain ⟨y, hxy, hyb⟩ := exists_between hxb

Result:
case intro.intro.h.mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
a✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[<] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
y : α
hxy : x < y
hyb : y < b
⊢ u ∈ atTop

Proof state:
case intro.intro.h.mp.intro.intro.intro.intro.intro.intro.intro.mk
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
a✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[<] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
y : α
hxy : x < y
hyb : y < b
z : α
hzs : z ∈ s
hyz : y ≤ z
⊢ ⟨z, hzs⟩ ∈ u

Tactic:
exact hts (hxt ⟨hxy.trans_le hyz, hb hzs⟩)

Result:
no goals

Proof state:
case intro.intro.h.mp.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
a✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[<] b
hts : Subtype.val ⁻¹' t ⊆ u
⊢ u ∈ atTop

Tactic:
obtain ⟨x, ⟨hxa : a ≤ x, hxb : x < b⟩, hxt : Ioo x b ⊆ t⟩ :=
  (mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset h).mp ht

Result:
case intro.intro.h.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
a✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
t : Set α
ht : t ∈ 𝓝[<] b
hts : Subtype.val ⁻¹' t ⊆ u
x : α
hxt : Ioo x b ⊆ t
hxa : a ≤ x
hxb : x < b
⊢ u ∈ atTop

Proof state:
case intro.intro.h
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
a✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
⊢ u ∈ comap Subtype.val (𝓝[<] b) ↔ u ∈ atTop

Tactic:
constructor

Result:
case intro.intro.h.mp
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
a✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
⊢ u ∈ comap Subtype.val (𝓝[<] b) → u ∈ atTop

case intro.intro.h.mpr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
a✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
⊢ u ∈ atTop → u ∈ comap Subtype.val (𝓝[<] b)

Proof state:
case intro.intro.h.mpr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
a✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
hu : u ∈ atTop
⊢ u ∈ comap Subtype.val (𝓝[<] b)

Tactic:
obtain ⟨x : s, hx : ∀ z, x ≤ z → z ∈ u⟩ := mem_atTop_sets.1 hu

Result:
case intro.intro.h.mpr.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b : α
s : Set α
hb : s ⊆ Iio b
hs✝ : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
a✝ : Nontrivial (Filter { x // x ∈ s })
this : Nonempty ↑s
a : α
h : a < b
hs : Ioo a b ⊆ s
u : Set { x // x ∈ s }
hu : u ∈ atTop
x : ↑s
hx : ∀ (z : ↑s), x ≤ z → z ∈ u
⊢ u ∈ comap Subtype.val (𝓝[<] b)