-- Mathlib/Topology/Separation/Regular.lean
theorem disjoint_nested_nhds [T3Space X] {x y : X} (h : x ≠ y) :
    ∃ U₁ ∈ 𝓝 x, ∃ V₁ ∈ 𝓝 x, ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y,
      IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
h : x ≠ y
U₁ U₂ : Set X
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
rcases exists_mem_nhds_isClosed_subset (U₁_op.mem_nhds x_in) with ⟨V₁, V₁_in, V₁_closed, h₁⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
h : x ≠ y
U₁ U₂ : Set X
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set X
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed V₁
h₁ : V₁ ⊆ U₁
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
h : x ≠ y
U₁ U₂ : Set X
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set X
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed V₁
h₁ : V₁ ⊆ U₁
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
rcases exists_mem_nhds_isClosed_subset (U₂_op.mem_nhds y_in) with ⟨V₂, V₂_in, V₂_closed, h₂⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
h : x ≠ y
U₁ U₂ : Set X
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set X
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed V₁
h₁ : V₁ ⊆ U₁
V₂ : Set X
V₂_in : V₂ ∈ 𝓝 y
V₂_closed : IsClosed V₂
h₂ : V₂ ⊆ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
h : x ≠ y
U₁ U₂ : Set X
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set X
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed V₁
h₁ : V₁ ⊆ U₁
V₂ : Set X
V₂_in : V₂ ∈ 𝓝 y
V₂_closed : IsClosed V₂
h₂ : V₂ ⊆ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
exact ⟨U₁, mem_of_superset V₁_in h₁, V₁, V₁_in, U₂, mem_of_superset V₂_in h₂, V₂, V₂_in,
  V₁_closed, V₂_closed, U₁_op, U₂_op, h₁, h₂, H⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
h : x ≠ y
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
rcases t2_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T3Space X
x y : X
h : x ≠ y
U₁ U₂ : Set X
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂