
Pigeonhole Principle
How many proofs are there for the pigeonhole principle? I know of one proof that just uses composition of functions to develop lemmas, and then ultimately come up with the Pigeonhole principle. The proof starts with the basic problem of 2 different ways of counting sets (i.e if $\displaystyle f: \mathbb{N}_{m} \to X $ and $\displaystyle f: \mathbb{N}_{n} \to X $ are bijections with the same codomain, then $\displaystyle m = n $). Namely, it says the following: Suppose that $\displaystyle X $ and $\displaystyle Y $ are finite, nonempty sets such that $\displaystyle X > Y$. Then $\displaystyle f: X \to Y $ is not an injection.

What is a finite set? It is a set such has no proper subset has a bijection with the full set. Use that fact and prove formally the principle.

There are several proofs as you observe. This of is found in many discrete mathematics texts.
Given that $\displaystyle m = \left X \right > \left Y \right = n$, recall that $\displaystyle
X = \bigcup\limits_{y \in Y} {\overleftarrow f \left\{ y \right\}} $.
Suppose that $\displaystyle \left( {\forall y \in Y} \right)\left[ {\left {\overleftarrow f \left\{ y \right\}} \right \le 1} \right]\quad$.
Using that we have $\displaystyle \left X \right = \left {\bigcup\limits_{y \in Y} {\overleftarrow f \left\{ y \right\}} } \right = \bigcup\limits_{y \in Y} {\left {\overleftarrow f \left\{ y \right\}} \right} \le n$ that is a contradiction.
Thus $\displaystyle \left( {\exists z \in Y} \right)\left[ {\left {\overleftarrow f \left\{ z \right\}} \right > 1} \right]$.
The value of this proof is that it also proves the generalized form. If we have m pigeons and n pigeonholes with $\displaystyle m > n$ the some hole contains at least $\displaystyle \left\lceil {\frac{m}{n}} \right\rceil $ pigeons (that is the ceiling function).
To see this proof use the assumptions above, using the supposition that $\displaystyle k = \left\lceil {\frac{m}{n}} \right\rceil \quad \& \quad \left( {\forall y \in Y} \right)\left[ {\left {\overleftarrow f \left\{ y \right\}} \right < k} \right]$.
This time $\displaystyle \left X \right = \left {\bigcup\limits_{y \in Y} {\overleftarrow f \left\{ y \right\}} } \right = \bigcup\limits_{y \in Y} {\left {\overleftarrow f \left\{ y \right\}} \right} \le n\left( {k  1} \right) \le m$ that is a contradiction.
Thus $\displaystyle \left( {\exists z \in Y} \right)\left[ {\left {\overleftarrow f \left\{ z \right\}} \right \ge k} \right]$.