obtain ⟨N, hN⟩ := Metric.tendsto_atTop.1 tendsto_one_div_add_atTop_nhds_0_nat (ε/2) (by linarith)
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε
case intro
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, dist (1 / (↑n + 1)) 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, 1 / (↑n + 1) ≤ ε