case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
obtain ⟨t, t_mem, ht⟩ : ∃ t ∈ f, t ×ˢ t ⊆ s := (cauchy_iff.1 hf).2 s hs
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ y, (x, y) ∈ s ∧ y ∈ t
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ t, t ∈ f ∧ t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
use t, t_mem, ht
no goals
case intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
f : Filter α
x : α
hf : Cauchy f
adhs : ClusterPt x f
s : Set (α × α)
hs : s ∈ 𝓤 α
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ s
⊢ ∃ y, (x, y) ∈ s ∧ y ∈ t
exact forall_mem_nonempty_iff_neBot.2 adhs _ (inter_mem_inf (mem_nhds_left x hs) t_mem)