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