How to formalize the below solution Ok so I have the following problem:
Let $f:[a,b]\to\mathbb{R}$ a continuos function with $f(a)=f(b)$. Show that there is an $x\in(a,b)$ and $(a_n)_n$ and $(b_n)_n$ sequences such that:
i) $a\leq a_n\leq b_n\leq b$
ii) $(a_n)_n$ is increasing while $(b_n)_n$ is decreasing
iii) both of the above sequences converge to $x$.
iv) $f(a_n)=f(b_n)$ for every natural $n$.
I want to know if there is some kind of formalization to the following heuristic I have:
Lemma: There exist $a<x<y<b$ with $f(x)=f(y)$.
Proof: Suppose the opposite. Then $f$ is injective on $(a,b)$ and since it is continuous it must be strictly monotone.But then $f(a)=\lim\limits_{x\to a}f(x)<\lim\limits_{x\to b}f(y)=f(b)$ or the other way around, which is a contradiction.
Now by the above lemma I can choose an increasing sequence $(a_n)_n$ and a decreasing one $(b_n)_n$ with $a_n<b_n$ and $f(a_n)=f(b_n)$ for every $n$.
If $a_{\omega}$ and $b_{\omega}$ are the limits of $(a_n)_n$ and $(b_n)_n$ then $f(a_{\omega})=f(b_{\omega})$ and so I can repeat the previous trick with ordinal numbers. This proccess must terminate with some ordinal $\alpha$ and $a_{\alpha}=b_{\alpha}$.
Now, by a lemma that seems to be true, but I haven't proved it yet, we can choose a increasing sequence of ordinals $\alpha_n$ with limit $\alpha$. Now, if we look at $a_{\alpha}$, $(a_{\alpha_n})_n$ and $(b_{\alpha_n})_n$, they satisfy the conditions.
I know that the above "solution" is kinda sloppy, but I am curious of a way of formalizing it, if there is one.
 A: Yes, this can be made precise (and true)! I would attack it as follows.
It will be helpful to introduce some terminology. Let's say that a trail is a pair of sequences $$\mathfrak{t}=\langle(a_i)_{i<\alpha}, (b_j)_{j<\alpha}\rangle$$ indexed by some ordinal $\alpha$ such that $a<a_i<a_{i+1}<b_{i+1}<b_i<b$ and $f(a_i)=f(b_i)$ for all $i<\alpha$. There is an obvious notion of extension of trails, and since the union of a chain of trails is again a trail Zorn's lemma tells us that there exists a (presumably non-unique!) non-"extendible" trail $\mathfrak{s}=\langle (u_i)_{i<\gamma},(v_i)_{i<\gamma}\rangle$. (changing up notation slightly to avoid possible mix-ups).
Now consider the sets $U=\{u_i:i<\gamma\}, V=\{v_i:i<\gamma\}$. These are bounded above and below respectively (in fact each is bounded both above and below), so by the completeness of $\mathbb{R}$ we have that $y:=\sup(U)$ and $z:=\inf(V)$ each exist. Clearly $y\le z$, and by continuity of $f$ we have $f(y)=f(z)$, but since $\mathfrak{s}$ is appropriately maximal we must not be able to "tack on" $y$ and $z$ to the left and right components of $\mathfrak{s}$ respectively to get a longer trail. This means that we must have $y=z$; let's take this point to be our $x$.
Now we need to extract a pair of length-$\omega$ sequences leading to $x$ from below and from above. The components of the maximal trail $\mathfrak{s}$ probably won't do, since the length of $\alpha$ might be much longer than $\omega$. However, it's at this point that a general topology fact comes into play:

$(*)\quad$ There is no order-preserving (or order-reversing) embedding of an uncountable ordinal into $\mathbb{R}$.

Consequently, the length $\gamma$ of $\mathfrak{s}$ must be a countable ordinal. Combined with the argument implicit in your post that this length must be a limit ordinal, we can extract a cofinal-in-$\gamma$ length-$\omega$ sequence $(\theta_i)_{i<\omega}$ of ordinals $<\gamma$; we'll then just set $$a_i=u_{\theta_i},\quad b_i=v_{\theta_i}.$$
Of course we still have to prove $(*)$, but this is a good exercise (think about how the countable set $\mathbb{Q}$ "sits inside" $\mathbb{R}$).

As a quick aside, my use of Zorn's lemma is - unsurprisingly - unnecessary, although it does simplify things. It's a fun, or perhaps "fun," exercise to modify the argument above so that no appeal to choice is used: by some cleverness involving $\mathbb{Q}$ we can actually build an explicit(ish) maximal trail, given appropriate $a,b,f$.
