Solution (source code)

= Solution
{c}

The <Bolzano-Weierstrass theorem> states that every <bounded sequence> of <real numbers> has a <convergent subsequence>. It is enough to select infinitely many terms of the <tangent> <sequence> that stay uniformly bounded.

For each positive <integer> $k$, choose $n_k=\lfloor k\pi+1/2\rfloor$, using the <floor function>. Then $|n_k-k\pi|\leq1/2$. Moreover $n_{k+1}-n_k\geq\pi-1>0$, so these are strictly increasing indices. By the period and <monotonicity> of the <tangent> on $(-\pi/2,\pi/2)$,
$$
|\tan n_k|=|\tan(n_k-k\pi)|\leq\tan(1/2).
$$
Thus $(\tan n_k)$ is a <bounded subsequence>. Applying the <Bolzano-Weierstrass theorem> to it gives a <convergent subsequence>, which is also a <subsequence> of the original <sequence>. \b[Such a <convergent subsequence> therefore exists.]