α : Type u_1
inst✝ : UniformSpace α
s✝ : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ (a, b) ∈ s
α : Type u_1
inst✝ : UniformSpace α
s : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
⊢ a = b
refine separated_def.1 s _ _ (fun s hs => ?_)
α : Type u_1
inst✝ : UniformSpace α
s✝ : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
s : Set (α × α)
hs : ∃ t, t ∈ 𝓤 (CauchyFilter α) ∧ (fun x => (pureCauchy x.fst, pureCauchy x.snd)) ⁻¹' t ⊆ s
⊢ (a, b) ∈ s
α : Type u_1
inst✝ : UniformSpace α
s✝ : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ (a, b) ∈ s
rw [← (@uniformEmbedding_pureCauchy α _).comap_uniformity, Filter.mem_comap] at hs
case intro.intro
α : Type u_1
inst✝ : UniformSpace α
s✝ : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
s : Set (α × α)
t : Set (CauchyFilter α × CauchyFilter α)
ht : t ∈ 𝓤 (CauchyFilter α)
hts : (fun x => (pureCauchy x.fst, pureCauchy x.snd)) ⁻¹' t ⊆ s
⊢ (a, b) ∈ s
α : Type u_1
inst✝ : UniformSpace α
s✝ : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
s : Set (α × α)
hs : ∃ t, t ∈ 𝓤 (CauchyFilter α) ∧ (fun x => (pureCauchy x.fst, pureCauchy x.snd)) ⁻¹' t ⊆ s
⊢ (a, b) ∈ s
obtain ⟨t, ht, hts⟩ := hs
no goals
case intro.intro
α : Type u_1
inst✝ : UniformSpace α
s✝ : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
s : Set (α × α)
t : Set (CauchyFilter α × CauchyFilter α)
ht : t ∈ 𝓤 (CauchyFilter α)
hts : (fun x => (pureCauchy x.fst, pureCauchy x.snd)) ⁻¹' t ⊆ s
⊢ (a, b) ∈ s
exact @hts (a, b) (Quotient.exact h t ht)