α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
⊢ (∀ (a b : α), (∀ (t : Set (α × α)), t ∈ (𝓤 α).sets → (a, b) ∈ t) ↔ a = b) ↔
    ∀ (x y : α), (∀ (r : Set (α × α)), r ∈ 𝓤 α → (x, y) ∈ r) → x = y
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
⊢ SeparatedSpace α ↔ ∀ (x y : α), (∀ (r : Set (α × α)), r ∈ 𝓤 α → (x, y) ∈ r) → x = y
simp only [separatedSpace_iff, Set.ext_iff, Prod.forall, mem_idRel, separationRel, mem_sInter]
no goals
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : UniformSpace α✝
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
⊢ (∀ (a b : α), (∀ (t : Set (α × α)), t ∈ (𝓤 α).sets → (a, b) ∈ t) ↔ a = b) ↔
    ∀ (x y : α), (∀ (r : Set (α × α)), r ∈ 𝓤 α → (x, y) ∈ r) → x = y
exact forall₂_congr fun _ _ => ⟨Iff.mp, fun h => ⟨h, fun H U hU => H ▸ refl_mem_uniformity hU⟩⟩