-- Mathlib/Topology/Separation/Regular.lean
theorem regularSpace_TFAE (X : Type u) [TopologicalSpace X] :
    List.TFAE [RegularSpace X,
      ∀ (s : Set X) x, x ∉ closure s → Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s,
      ∀ (x : X) (s : Set X), s ∈ 𝓝 x → ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s,
      ∀ x : X, (𝓝 x).lift' closure ≤ 𝓝 x,
      ∀ x : X , (𝓝 x).lift' closure = 𝓝 x]

Proof state:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure s
ha' : sᶜ ∈ 𝓝 a
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩

Result:
case intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed U
hUs : U ⊆ sᶜ
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s,
      ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x, ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x].TFAE

Tactic:
tfae_have 1 ↔ 5 := by
  rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_swap]
  simp only [isClosed_compl_iff, mem_compl_iff, Classical.not_not, @and_comm (_ ∈ _),
    (nhds_basis_opens _).lift'_closure.le_basis_iff (nhds_basis_opens _), and_imp,
    (nhds_basis_opens _).disjoint_iff_right, exists_prop, ← subset_interior_iff_mem_nhdsSet,
    interior_compl, compl_subset_compl]

Result:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s,
      ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x, ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x].TFAE

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ (∀ (y : X) (x : Set X), IsClosed xᶜ → y ∉ xᶜ → Disjoint (𝓝ˢ xᶜ) (𝓝 y)) ↔ ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x

Tactic:
simp only [isClosed_compl_iff, mem_compl_iff, Classical.not_not, @and_comm (_ ∈ _),
  (nhds_basis_opens _).lift'_closure.le_basis_iff (nhds_basis_opens _), and_imp,
  (nhds_basis_opens _).disjoint_iff_right, exists_prop, ← subset_interior_iff_mem_nhdsSet,
  interior_compl, compl_subset_compl]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s) → ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x)
tfae_2_to_3 :
  (∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x)) → ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s,
      ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x, ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x].TFAE

Tactic:
tfae_have 3 → 1 := fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩

Result:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s) → ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x)
tfae_2_to_3 :
  (∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x)) → ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s
tfae_3_to_1 : (∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s) → RegularSpace X
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s,
      ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x, ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x].TFAE

Proof state:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
tfae_4_to_2 :
  (∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s) → ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x)
tfae_2_to_3 :
  (∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x)) → ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s
tfae_3_to_1 : (∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s) → RegularSpace X
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s,
      ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x, ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s,
      ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x, ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x].TFAE

Tactic:
tfae_have 5 → 6 := fun h a => (h a).antisymm (𝓝 _).le_lift'_closure

Result:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s,
      ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x, ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x].TFAE

Proof state:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure = 𝓝 x
tfae_6_to_4 : (∀ (x : X), (𝓝 x).lift' closure = 𝓝 x) → ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure s
⊢ sᶜ ∈ 𝓝 a

Tactic:
rwa [← mem_interior_iff_mem_nhds, interior_compl]

Result:
no goals