case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T3Space α
x y : α
h : x ≠ y
U₁ U₂ : Set α
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
⊢ ∃ U₁,
    U₁ ∈ 𝓝 x ∧
      ∃ V₁,
        V₁ ∈ 𝓝 x ∧
          ∃ U₂,
            U₂ ∈ 𝓝 y ∧
              ∃ V₂, V₂ ∈ 𝓝 y ∧ IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T3Space α
x y : α
h : x ≠ y
⊢ ∃ U₁,
    U₁ ∈ 𝓝 x ∧
      ∃ V₁,
        V₁ ∈ 𝓝 x ∧
          ∃ U₂,
            U₂ ∈ 𝓝 y ∧
              ∃ V₂, V₂ ∈ 𝓝 y ∧ IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
rcases t2_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T3Space α
x y : α
h : x ≠ y
U₁ U₂ : Set α
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set α
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed V₁
h₁ : V₁ ⊆ U₁
⊢ ∃ U₁,
    U₁ ∈ 𝓝 x ∧
      ∃ V₁,
        V₁ ∈ 𝓝 x ∧
          ∃ U₂,
            U₂ ∈ 𝓝 y ∧
              ∃ V₂, V₂ ∈ 𝓝 y ∧ IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T3Space α
x y : α
h : x ≠ y
U₁ U₂ : Set α
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
⊢ ∃ U₁,
    U₁ ∈ 𝓝 x ∧
      ∃ V₁,
        V₁ ∈ 𝓝 x ∧
          ∃ U₂,
            U₂ ∈ 𝓝 y ∧
              ∃ V₂, V₂ ∈ 𝓝 y ∧ IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
rcases exists_mem_nhds_isClosed_subset (U₁_op.mem_nhds x_in) with ⟨V₁, V₁_in, V₁_closed, h₁⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T3Space α
x y : α
h : x ≠ y
U₁ U₂ : Set α
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set α
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed V₁
h₁ : V₁ ⊆ U₁
V₂ : Set α
V₂_in : V₂ ∈ 𝓝 y
V₂_closed : IsClosed V₂
h₂ : V₂ ⊆ U₂
⊢ ∃ U₁,
    U₁ ∈ 𝓝 x ∧
      ∃ V₁,
        V₁ ∈ 𝓝 x ∧
          ∃ U₂,
            U₂ ∈ 𝓝 y ∧
              ∃ V₂, V₂ ∈ 𝓝 y ∧ IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T3Space α
x y : α
h : x ≠ y
U₁ U₂ : Set α
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set α
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed V₁
h₁ : V₁ ⊆ U₁
⊢ ∃ U₁,
    U₁ ∈ 𝓝 x ∧
      ∃ V₁,
        V₁ ∈ 𝓝 x ∧
          ∃ U₂,
            U₂ ∈ 𝓝 y ∧
              ∃ V₂, V₂ ∈ 𝓝 y ∧ IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
rcases exists_mem_nhds_isClosed_subset (U₂_op.mem_nhds y_in) with ⟨V₂, V₂_in, V₂_closed, h₂⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T3Space α
x y : α
h : x ≠ y
U₁ U₂ : Set α
U₁_op : IsOpen U₁
U₂_op : IsOpen U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set α
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed V₁
h₁ : V₁ ⊆ U₁
V₂ : Set α
V₂_in : V₂ ∈ 𝓝 y
V₂_closed : IsClosed V₂
h₂ : V₂ ⊆ U₂
⊢ ∃ U₁,
    U₁ ∈ 𝓝 x ∧
      ∃ V₁,
        V₁ ∈ 𝓝 x ∧
          ∃ U₂,
            U₂ ∈ 𝓝 y ∧
              ∃ V₂, V₂ ∈ 𝓝 y ∧ IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
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⟩