intros ε ε_pos
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
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| < ε
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(u ∘ φ) n - c| ≤ ε