-- Mathlib/Topology/Order/Basic.lean
theorem mem_nhds_iff_exists_Ioo_subset' [OrderTopology α] {a : α} {s : Set α} (hl : ∃ l, l < a)
    (hu : ∃ u, a < u) : s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Proof state:
case mpr.intro.intro.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
l u : α
ha : a ∈ Ioo l u
h : Ioo l u ⊆ s
⊢ s ∈ 𝓝 a

Tactic:
apply mem_of_superset (Ioo_mem_nhds ha.1 ha.2) h

Result:
no goals

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
constructor

Result:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a → ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a

Proof state:
case mp.intro.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩

Result:
case mp.intro.intro.intro.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl✝ : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
l : α
la : l < a
hl : Ioc l a ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Proof state:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a → ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
intro h

Result:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
h : s ∈ 𝓝 a
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Proof state:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
h : s ∈ 𝓝 a
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩

Result:
case mp.intro.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Proof state:
case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a

Tactic:
rintro ⟨l, u, ha, h⟩

Result:
case mpr.intro.intro.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
l u : α
ha : a ∈ Ioo l u
h : Ioo l u ⊆ s
⊢ s ∈ 𝓝 a

Proof state:
case mp.intro.intro.intro.intro
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl✝ : ∃ l, l < a
hu✝ : ∃ u, a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
l : α
la : l < a
hl : Ioc l a ⊆ s
⊢ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
exact ⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩

Result:
no goals