simp_rw [Metric.tendsto_nhds, eventually_atTop, Real.dist_eq] at lim
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)
⊢ seq_limit (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 : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
⊢ seq_limit (u ∘ φ) c