Let $T: X \to X$ be a continuous map on a compact metric space $X$. We say $T$ is distal if $\inf_n d(T^n x, T^n y) = 0$ implies $x = y$.
Then it is true that $T$ is bijective.
Question: Is there an elementary proof of this fact? (Injectivity clearly follows, surjectivity is the issue.) The two proofs I know go through the enveloping semigroup, and the Stone-Čech compactification $\beta \mathbb N$ respectively.
The answer is yesser than I thought. I mentioned this issue at http://eventos.cmm.uchile.cl/edynamicsxiii/, since the proximality lemma from my previous answer was discussed there. Someone pointed out that Hindman's original proof of his famous theorem is at least somewhat elementary in some technical sense, and implies a significant part of the proximality theorem, so the answer must be "yes" at least in some technical sense.
After a bit of searching I found the relevant paper [1]: in the sense of reverse mathematics, your theorem is provable in $\mathrm{ACA}_0^+$, a certain fragment of second-order arithmetic.
I quote the relevant theorem in the form stated in this paper. They call this the Auslander-Ellis theorem.
Theorem. Let $X$ be a compact metric space and let $T : X \to X$ be continuous. Regard $(X,T)$ as dynamical system. Given $x \in X$, there exists $y \in X$ such that $y$ is uniformly recurrent and proximal to $x$.
They show that this theorem is provable in $\mathrm{ACA}_0^+$. Let me recall how to conclude your result (this deduction seems very elementary, so I guess it needs much less than $\mathrm{ACA}_0^+$).
Corollary. Every distal system is invertible.
Proof. Injectivity is clear. Take $x \in X$, and apply the previous theorem, to get that $x$ is proximal to some uniformly recurrent $y$. Then $x = y$, so every point in $X$ is uniformly recurrent. Clearly this implies surjectivity, since if $U$ is a neighborhood of any $x \in X$, we have $T^n(x) \in U$ for some positive $n$, and then $T^{n-1}(x)$ maps to $U$ in $T$, so $TX$ is dense in $X$ and by compactness is equal to $X$. Square.
I am not an expert, but as far as I understand, second-order arithmetic in itself is weaker than Zermelo-Frankel set theory (without choice), and $\mathrm{ACA}_0^+$ is about medium strength as far as the most commonly studied fragments of second-order arithmetic go. Roughly, the logic $\mathrm{ACA}_0$ says that a set of natural numbers exists if you can define it by an arithmetical formula, and $\mathrm{ACA}_0^+$ adds the $\omega$th Turing jump of each set already definable.
Nevertheless, to quote [1], "It is well known that all existing proofs of HT are nonconstructive. One of the goals of this paper is to delimit the degree of nonconstructivity which is inherent in Hindman's Theorem."
To summarize the logical connections obtained: Write AET for the theorem about proximality, HT for Hindman's theorem, DT for OP's theorem about distal systems. We have $$\mathrm{ACA_0^+} \implies \mathrm{AET} \implies \mathrm{HT} \implies \mathrm{ACA_0} \wedge \mathrm{DT}$$ Intuitively (and again I am not an expert), if you believe results of a certain flavor of infinite computation are well-defined, you can prove AET and therefore the theorem about distal systems. But in theory, the problem about distal systems could be much easier (I have a hard time imagining a proof not going through proximal pairs, but I've been wrong before). In the reverse math framework, one could ask if it is in $\mathrm{ACA}_0$, or $\mathrm{WKL}_0$, or $\mathrm{RCA}_0$, in decreasing order of strength.
Reference
[1]: Blass, Andreas R.; Hirst, Jeffry L.; Simpson, Stephen G., Logical analysis of some theorems of combinatorics and topological dynamics, Logic and combinatorics, Proc. AMS-IMS-SIAM Conf., Arcata/Calif. 1985, Contemp. Math. 65, 125-156 (1987). ZBL0652.03040.
It is a very nice result ! Let me try an "elementary" answer.
Define $\delta: X\times X \to \mathbb R_+$ by $$\delta(x,y)= \inf_{n\in \mathbb N} d(T^n(x), T^n(y))~.$$ This function is continuous and vanishes exactly on the diagonal by distality.
Edit: This function is NOT continuous in general, as pointed out in the comments.
Set $$F= \bigcap_{n\in \mathbb N} T^n(X)~.$$ $F$ is compact and for all $x\in X$ we have $d(T^n(x), F) \underset{n\to +\infty} \longrightarrow 0$. Since $$\inf_{y\in F} \delta(x,y) \leq \inf_{y\in F} d(T^n(x),y)$$ for all $n$, we conclude that $$\inf_{y\in F} \delta(x,y) = 0~.$$
By compactness of $F$ and distality, we conclude that $x\in F$ for all $x$. Hence $F=X$ and $T$ is surjective.
Edit: Of course this last line falls appart if $\delta$ is not continuous. So the question is: why is the infimum $\inf_{y\in F} \delta(x,y) = 0$ is attained ?
edit
My appeal to authority in the following answer makes no sense, because it seems Auslander's flows are actually assumed to be invertible. My own intuition is still that the issue is the same, so I'll keep this for now.
original
I also did not understand why $\delta$ is continuous in the answer of Nicolas Tholozan, maybe they will clarify and I'll delete this, but in the meantime, I would have guessed this has no known elementary proof (or at least didn't in '88...) for the following reason: The only proof I can see is through the following theorem on page 67 in Auslander's '88 book Minimal Flows and their Extensions (in the chapter on distal flows):
Let $(X, T)$ be a flow and let $x \in X$. Then there is an almost periodic point $x^*$ which is proximal to $x$.
Your result easily follows, because the almost periodic point will be in the eventual image. Auslander makes the following comment after the theorem:
"Every known proof of this theorem requires the use of a "large" product space (another proof will be given in the next chapter). It would be interesting to find a direct proof."
I don't see a reduction of this to the result you are after, so possibly yours is easier, but this was the only reasonable approach I could see. I also don't know if Auslander's comment has already been addressed somewhere, I am not an expert on distality by any means.
