-- Mathlib/Topology/Inseparable.lean
theorem specializes_TFAE (x y : X) :
    TFAE [x ⤳ y,
      pure x ≤ 𝓝 y,
      ∀ s : Set X , IsOpen s → y ∈ s → x ∈ s,
      ∀ s : Set X , IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure ({ x } : Set X),
      closure ({ y } : Set X) ⊆ closure { x },
      ClusterPt y (pure x)]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE

Tactic:
tfae_have 6 ↔ 5 := isClosed_closure.closure_subset_iff.trans singleton_subset_iff

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE

Tactic:
tfae_have 3 → 4 := fun h s hsc hx => of_not_not fun hy => h sᶜ hsc.isOpen_compl hy hx

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
tfae_5_iff_7 : y ∈ closure {x} ↔ ClusterPt y (pure x)
⊢ y ∈ closure {x} → x ⤳ y

Tactic:
refine fun h => (nhds_basis_opens _).ge_iff.2 ?_

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
tfae_5_iff_7 : y ∈ closure {x} ↔ ClusterPt y (pure x)
h : y ∈ closure {x}
⊢ ∀ (i' : Set X), y ∈ i' ∧ IsOpen i' → i' ∈ 𝓝 x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
tfae_6_iff_5 : closure {y} ⊆ closure {x} ↔ y ∈ closure {x}
⊢ y ∈ closure {x} ↔ ClusterPt y (pure x)

Tactic:
rw [mem_closure_iff_clusterPt, principal_singleton]

Result:
no goals

Proof state:
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
y : X
s : Set X
hy : y ∈ s
ho : IsOpen s
z : X
hxs : z ∈ s
tfae_1_to_2 : z ⤳ y → pure z ≤ 𝓝 y
tfae_2_to_3 : pure z ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → z ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → z ∈ s) → ∀ (s : Set X), IsClosed s → z ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → z ∈ s → y ∈ s) → y ∈ closure {z}
tfae_6_iff_5 : closure {y} ⊆ closure {z} ↔ y ∈ closure {z}
tfae_5_iff_7 : y ∈ closure {z} ↔ ClusterPt y (pure z)
h : y ∈ closure {z}
⊢ s ∈ 𝓝 z

Tactic:
exact ho.mem_nhds hxs

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE

Tactic:
tfae_have 4 → 5 := fun h => h _ isClosed_closure (subset_closure <| mem_singleton _)

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) → y ∈ closure {x}
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE