How long does a sequence need to be to be guaranteed to have a monotonic subsequence length k?

Let us prove the following theorem by using pigeonhole principle.

Theorem: If you place $1,2,\cdots, n^2+1$ in a row in arbitrary order, then there exists a monotonic(increasing or decreasing) sequence with length equal to or more than $n+1$.

Proof : Let $a_1,a_2,\cdots,a_{n^2+1}$ be the numbers in a row. Also, let $inc[i]$ be the length of the maximum increasing sequence from $a_i$, and let $dec[i]$ be the length of the maximum decreasing sequence from $a_i$.

Then, for $i=1,2,\cdots, n^2+1$, let us consider the lattice point $(inc[i],dec[i])$. If either $inc[i]$ or $dec[i]$ is equal to or more than $n+1$, then we are happy. So, let us suppose this situation does not happen.

Then, since $n^2+1$ points are set in the $n^2$ points from $(1,1)$ to $(n,n)$, by pigeonhole principle, there exists at least one pair of distinct integers $i,j$ such that $$(inc[i],dec[i])=(inc[j],dec[j])$$

However, this never happens. This is because if $i\lt j$, then either $a_i\lt a_j$ or $a_i\gt a_j$ holds. The former leas $inc[i]\lt inc[j]$, the latter leads $dec[i]\gt dec[j].$ Then, we now know the supposition leads a contradiction.

Hence, we now know that either $inc[i]$ or $dec[i]$ is equal to or more than $n+1$. This is what we have to show. Q.E.D.

The search term for background on the question and the other answers is

Erdos-Szekeres theorem (on monotone subsequences).

The theorem, with several remarkable proofs and generalizations, is that a sequence of length $mn+1$ has an increasing subsequence $m+1$ long, or a length $n+1$ decreasing subsequence.

To the stated question,

How long does a sequence need to be to be guaranteed to have a monotonic subsequence length $k$?

the answer is that the E-S bound of $mn+1$ is the minimum needed to guarantee $(m+1,n+1)$. Thus for $(n,n)$ the minimum length is $(n-1)^2+1$ and there are sequences of length $(n-1)^2$ with no monotone subsequence of length $n$. Earlier question on that:

Why is Erdős–Szekeres theorem sharp?

I like the proof based on Dilworth's theorem. It is the sixth proof in section 2 of this delightful overview. A finite partial order of at least $n^2+1$ elements contains either a chain or an anti-chain of length $n+1$. Apply this to the coordinate-wise partial order on the pairs $(k, a_k)$ where $a$ is a sequence of length at least $n^2+1$.