-- Mathlib/Topology/Separation/Basic.lean
theorem isOpen_inter_eq_singleton_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X}
    (hx : x ∈ s) : ∃ U : Set X, IsOpen U ∧ U ∩ s = {x}

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
t : Set X
ht_sub : t ⊆ U
ht_open : IsOpen t
ht_x : x ∈ t
⊢ ∃ U, IsOpen U ∧ U ∩ s = {x}

Tactic:
refine ⟨t, ht_open, Set.Subset.antisymm ?_ ?_⟩

Result:
case intro.intro.intro.intro.intro.refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
t : Set X
ht_sub : t ⊆ U
ht_open : IsOpen t
ht_x : x ∈ t
⊢ t ∩ s ⊆ {x}

case intro.intro.intro.intro.intro.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
t : Set X
ht_sub : t ⊆ U
ht_open : IsOpen t
ht_x : x ∈ t
⊢ {x} ⊆ t ∩ s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
⊢ ∃ U, IsOpen U ∧ U ∩ s = {x}

Tactic:
obtain ⟨U, hU_nhds, hU_inter⟩ := nhds_inter_eq_singleton_of_mem_discrete hx

Result:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
⊢ ∃ U, IsOpen U ∧ U ∩ s = {x}

Proof state:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
⊢ ∃ U, IsOpen U ∧ U ∩ s = {x}

Tactic:
obtain ⟨t, ht_sub, ht_open, ht_x⟩ := mem_nhds_iff.mp hU_nhds

Result:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
t : Set X
ht_sub : t ⊆ U
ht_open : IsOpen t
ht_x : x ∈ t
⊢ ∃ U, IsOpen U ∧ U ∩ s = {x}

Proof state:
case intro.intro.intro.intro.intro.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
t : Set X
ht_sub : t ⊆ U
ht_open : IsOpen t
ht_x : x ∈ t
⊢ x ∈ t ∧ x ∈ s

Tactic:
exact ⟨ht_x, hx⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
t : Set X
ht_sub : t ⊆ U
ht_open : IsOpen t
ht_x : x ∈ t
⊢ {x} ⊆ t ∩ s

Tactic:
rw [Set.subset_inter_iff, Set.singleton_subset_iff, Set.singleton_subset_iff]

Result:
case intro.intro.intro.intro.intro.refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
t : Set X
ht_sub : t ⊆ U
ht_open : IsOpen t
ht_x : x ∈ t
⊢ x ∈ t ∧ x ∈ s

Proof state:
case intro.intro.intro.intro.intro.refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
t : Set X
ht_sub : t ⊆ U
ht_open : IsOpen t
ht_x : x ∈ t
⊢ t ∩ s ⊆ {x}

Tactic:
exact hU_inter ▸ Set.inter_subset_inter_left s ht_sub

Result:
no goals