-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem TFAE_mem_nhdsGT {a b : α} (hab : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[>] a,
      s ∈ 𝓝[Ioc a b] a,
      s ∈ 𝓝[Ioo a b] a,
      ∃ u ∈ Ioc a b, Ioo a u ⊆ s,
      ∃ u ∈ Ioi a, Ioo a u ⊆ s]

Proof state:
case intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
x✝ : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := x✝
v : Set α
va : v ∈ 𝓝 a
hv : v ∩ Ioi a ⊆ s
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
x✝ : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := x✝
v : Set α
va : v ∈ 𝓝 a
hv : v ∩ Ioi a ⊆ s
u : α
au : u ∈ Ioc a b
hu : Ico a u ⊆ v
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a

Tactic:
rw [nhdsWithin_Ioo_eq_nhdsGT hab]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
tfae_1_to_4 : s ∈ 𝓝[>] a → ∃ u ∈ Ioc a b, Ioo a u ⊆ s
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Tactic:
tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
x✝ : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := x✝
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩

Result:
case intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
x✝ : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := x✝
v : Set α
va : v ∈ 𝓝 a
hv : v ∩ Ioi a ⊆ s
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a

Tactic:
rw [nhdsWithin_Ioc_eq_nhdsGT hab]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Tactic:
tfae_have 1 ↔ 2 := by
  rw [nhdsWithin_Ioc_eq_nhdsGT hab]

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Tactic:
tfae_have 1 ↔ 3 := by
  rw [nhdsWithin_Ioo_eq_nhdsGT hab]

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
x✝ : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := x✝
v : Set α
va : v ∈ 𝓝 a
hv : v ∩ Ioi a ⊆ s
u : α
au : u ∈ Ioc a b
hu : Ico a u ⊆ v
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
exact ⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Tactic:
tfae_have 5 → 1
| ⟨u, hau, hu⟩ => mem_of_superset (Ioo_mem_nhdsGT hau) hu

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE