A proof of $|\mathbb{N}| = |\mathbb{N} \times \mathbb{N}|$ $\newcommand{\N}{\mathbb{N}}$
There are various versions of proof of 'there is a bijection from $\N$ to $\N \times \N$.' But only one of them suits my taste: Make a list
$$
\begin{aligned}
&(1,1),\\
&(1,2), (2,1)\\
&(1,3), (2,2),...
\end{aligned}
$$
and index them by $\N = \{1,2,\cdots\}$. The sum of the elements of each pair equals the index of the corresponding layer plus $1$. It provides the key idea, but I feel I need to explicitly show that it really works. Please check if the followings are valid.
First, let us restrict the domain of discourse to natural numbers. I defined a function $f: \N \to \N^2$ with
$$
\forall m :\forall n \le m:f\left(\frac{(m-1)m}{2} + n\right) = (n,m-n+1)
$$
where $m$ is the index for each layer of the list and $n$ is the column index. $(m-1)m/2$ can be thought of as the accumulated number of elements from the first layer and the layer $m-1$.
Now, we have to show $f$ is bijective.

*

*(surjective) I am going to show that $\forall a, b: \exists k:f(k) = (a,b)$. Let $n = a$, and $m-n+1 = b$. Then,
$$
m = n + b - 1 \ge n
$$
Letting $ k = (a + b - 2)(a + b - 1)/2 + a$ shows $f$ is subjective.


*(uniqueness of $m$ and $n$ for each argument $k$ of $f$) First, we show that
$$
\forall k: \exists!m,n: \left(n \le m \land k = \frac{(m-1)m}{2} + n\right)
$$
It is easy to show that
$$
\left\{\left.\left(\frac{(m-1)m}{2}\right.,\left.\frac{m(m+1)}{2}\right]\cap\N ~\right|~m\in\N \right\}
$$
partitions $\N$. Therefore, for arbitrary $k$, there is unique $m$ such that
$$
\frac{(m-1)m}{2} < k \le \frac{m(m+1)}{2}
\text{ or equivalently, }
0 < k - \frac{(m-1)m}{2} \le m
$$
Using the result, let $n = k - {(m-1)m}/{2} $.


*(injective) It follows from 2) that for each $a, b \in \N$ there is unique $k$ such that $f(k) = (a,b)$.
The proof is a lot verbose, but I could be content only with such details.

All the details are in the Wikipedia page for this Cantor's pairing. It even derives an inverse.
But IMO $f(n,m)=2^{n-1}\cdot (2m-1)$ is a simpler bijection from $\Bbb N \times \Bbb N$ to $\Bbb N$ ($\Bbb N=\{1,2,3,\ldots\}$) (from my high school days). It's based on the simple observation that every number is a power of $2$ (possibly $2^0=1$) times an odd number in a unique way.
