-- Mathlib/Topology/UniformSpace/Separation.lean
theorem isClosed_of_spaced_out [T0Space α] {V₀ : Set (α × α)} (V₀_in : V₀ ∈ 𝓤 α) {s : Set α}
    (hs : s.Pairwise fun x y => (x, y) ∉ V₀) : IsClosed s

Proof state:
case intro.intro.intro.h.intro.intro.h
α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y => (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
⊢ (x, y) ∈ V

Tactic:
rcases hx (inter_mem V₁_in V_in) with ⟨z, hz, hz'⟩

Result:
case intro.intro.intro.h.intro.intro.h.intro.intro
α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y => (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ (x, y) ∈ V

Proof state:
α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y => (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ z = y

Tactic:
by_contra hzy

Result:
α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y => (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SymmetricRel V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hzy : ¬z = y
⊢ False

Proof state:
case intro.intro.intro.h.intro.intro
α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y => (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ x ∈ s

Tactic:
suffices x = y by rwa [this]

Result:
case intro.intro.intro.h.intro.intro
α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y => (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
⊢ x = y

Proof state:
α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y => (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SymmetricRel V₁
h_comp : V₁ ○ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
this : x = y
⊢ x ∈ s

Tactic:
rwa [this]

Result:
no goals