Theorem: cluster_limit (GlimpseOfLean/Exercises/Topics/SequenceLimits.lean)

State before:
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
ha : cluster_point u a
⊢ a = l
Tactic:
sorry
State after:
no goals