rcases (isCompact_Icc : IsCompact (Icc a b)).tendsto_subseq h with ⟨c, c_in, φ, hφ, lim⟩
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
⊢ ∃ c ∈ Icc a b, cluster_point u c
case intro.intro.intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : Tendsto ((fun n => u n) ∘ φ) atTop (nhds c)
⊢ ∃ c ∈ Icc a b, cluster_point u c