[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
⊢ a ∈ s
[PROOFSTEP]
let f := 𝓝[s] a
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
⊢ a ∈ s
[PROOFSTEP]
have : Cauchy f := cauchy_nhds.mono' ha inf_le_left
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
⊢ a ∈ s
[PROOFSTEP]
rcases h f this inf_le_right with ⟨y, ys, fy⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
y : α
ys : y ∈ s
fy : f ≤ 𝓝 y
⊢ a ∈ s
[PROOFSTEP]
rwa [(tendsto_nhds_unique' ha inf_le_left fy : a = y)]
