rcases hyp with ⟨φ, φ_extr, hφ⟩
u : ℕ → ℝ
a : ℝ
hyp : cluster_point u a
ε : ℝ
ε_pos : ε > 0
N : ℕ
⊢ ∃ n ≥ N, |u n - a| ≤ ε
case intro.intro
u : ℕ → ℝ
a ε : ℝ
ε_pos : ε > 0
N : ℕ
φ : ℕ → ℕ
φ_extr : extraction φ
hφ : seq_limit (u ∘ φ) a
⊢ ∃ n ≥ N, |u n - a| ≤ ε