-- Mathlib/Topology/Separation/Basic.lean
theorem t1Space_TFAE (X : Type u) [TopologicalSpace X] :
    List.TFAE [T1Space X,
      ∀ x, IsClosed ({ x } : Set X),
      ∀ x, IsOpen ({ x }ᶜ : Set X),
      Continuous (@CofiniteTopology.of X),
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y]

Proof state:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed {x}) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ [T1Space X, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}ᶜ, Continuous ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y].TFAE

Tactic:
tfae_have 1 → 4 := by
  simp only [continuous_def, CofiniteTopology.isOpen_iff']
  rintro H s (rfl | hs)
  exacts [isOpen_empty, compl_compl s ▸ (@Set.Finite.isClosed _ _ H _ hs).isOpen_compl]

Result:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed {x}) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space X → Continuous ⇑CofiniteTopology.of
⊢ [T1Space X, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}ᶜ, Continuous ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y].TFAE

Proof state:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed {x}) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

Tactic:
simp only [(nhds_basis_opens _).mem_iff, subset_compl_singleton_iff, exists_prop, and_assoc,
  and_left_comm]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed {x}) ↔ ∀ (x : X), IsOpen {x}ᶜ
⊢ (∀ (y x : X), x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen {x}ᶜ

Tactic:
simp only [isOpen_iff_mem_nhds, mem_compl_iff, mem_singleton_iff]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed {x}) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
⊢ T1Space X → ∀ (s : Set (CofiniteTopology X)), s = ∅ ∨ sᶜ.Finite → IsOpen (⇑CofiniteTopology.of ⁻¹' s)

Tactic:
rintro H s (rfl | hs)

Result:
case inl
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed {x}) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space X
⊢ IsOpen (⇑CofiniteTopology.of ⁻¹' ∅)

case inr
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed {x}) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen (⇑CofiniteTopology.of ⁻¹' s)