This PR changes the definition of regular_space, requesting only the t0_space condition, instead of the t1_space that was asked before.

class regular_space (α : Type u) [topological_space α] extends t0_space α : Prop :=
(regular : ∀{s:set α} {a}, is_closed s → a ∉ s → ∃t, is_open t ∧ s ⊆ t ∧ 𝓝[t] a = ⊥)

Due to that change, I also had to reformulate the proof of the lemma separed_regular in src/topology/uniform_space/separation.lean adding the T₀ condition. I have also defined the Uryson space, with their respective lemmas about the relations with T₂ and T₃, and, finally, prove the relation between the definition of t1_space from mathlib and the common definition with open sets.

lemma t1_iff_exists_open : t1_space α ↔
  ∀ (x y), x ≠ y → (∃ (U : set α) (hU : is_open U), x ∈ U ∧ y ∉ U) :=
begin
  split,
  { introsI t1 x y hxy,
    exact ⟨{y}ᶜ, is_open_compl_iff.mpr (t1_space.t1 y),
            mem_compl_singleton_iff.mpr hxy,
            not_not.mpr rfl⟩},
  { intro h,
    constructor,
    intro x,
    rw ← is_open_compl_iff,
    have p : ⋃₀ {U : set α | (x ∉ U) ∧ (is_open U)} = {x}ᶜ,
    { apply subset.antisymm; intros t ht,
      { rcases ht with ⟨A, ⟨hxA, hA⟩, htA⟩,
        rw [mem_compl_eq, mem_singleton_iff],
        rintro rfl,
        contradiction },
      { obtain ⟨U, hU, hh⟩ := h t x (mem_compl_singleton_iff.mp ht),
        exact ⟨U, ⟨hh.2, hU⟩, hh.1⟩}},
    rw ← p,
    exact is_open_sUnion (λ B hB, hB.2) }
end

If you want to see the original Pull Request at the Mathlib Repository you can do it here.