cases' hl' with N' hN'
case a.intro
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
hl' : ∃ N, ∀ n ≥ N, |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε
case a.intro.intro
u : ℕ → ℝ
l l' ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε / 2
N' : ℕ
hN' : ∀ n ≥ N', |u n - l'| ≤ ε / 2
⊢ |l - l'| ≤ ε