So now I managed to put together a couple of proofs, that each of them use a similar procedure in a crucial step, and I am not sure what are the requirements for this step to be true.
First example:
Proving the metric space $B(X,\Bbb{R})=\{f:X\to \Bbb{R}: f \text{ is bounded}\}$ with $d_{\infty}(f,g)=\sup_{x \in X}|f(x)-g(x)|$) is complete.
Since my question is not about the proof in general, but about the step im going to mention, I will omit the proof, (if it is not clear, I will just add it).
The thing is we have a Cauchy sequence $(f_n)\subset B(X,\Bbb{R})$ and we want to see that $(f_n)$ is actually convergent. So for any given $x\in X$, you can easily see that $(f_n(x))\subset \Bbb{R}$ is Cauchy and therefore $f_n(x) \to f(x) \in \Bbb{R}$.
So the argument they use is
$$d_{\infty}(f_n,f_m)=\sup_{x \in X}|f_n(x)-f_m(x)|<\epsilon$$
So making $m\to \infty$ we have that $\sup_{x \in X}|f_n(x)-f(x)|\leq \epsilon$
So basically what is going on is that they are "inserting" the taking limit operation inside the module, which is maybe (definetely not for me) perfectly acceptable.
Another example, of "limit taking insertion" is given in Proving $\ell^p$ is complete. Were the user proceeds in this way, three times, and in three different ways.
My question is: can you always take limits freely, fixing the other variables? What are they taking into account when doing this?
Great question. I wondered that myself too, a while back. Let's put in the middle steps. We have: $$\sup_{x \in X}|f_n(x)-f_m(x)| < \epsilon, \stackrel{m \to +\infty}{\implies} \sup_{x \in X}|f_n(x)-f(x)| \leq \epsilon.$$But all the details are: given $\epsilon > 0$, there exists $n_0 \in \Bbb Z_{>0}$ such that: $$\sup_{x \in X}|f_n(x) - f_m(x)| < \epsilon, \quad \forall\,n,m \geq n_0.$$Definition of $(f_n)_{n \geq 0}$ being a Cauchy sequence, nothing new under the sun. This means that: $$|f_n(x)-f_m(x)| < \epsilon\quad \forall\,m,n \geq n_0,\quad \forall\,x \in X,$$ because of the definition of $\sup_{x \in X}$. Now, because of the $\forall\,m \geq n_0$ bit, we can make $m \to +\infty$. If that were valid just for a few $m$'s, we couldn't do the limit process. With this: $$\lim_{m \to +\infty}|f_n(x)-f_m(x)| \leq \epsilon, \quad \forall\,n \geq n_0,\quad \forall\,x \in X.$$ Notice how $\forall\,m \geq n_0$ is gone now. Now, I can swap $\lim_{m \to +\infty}$ with $|\cdot|$, because $|\cdot|$ is a continuous function. Now: $$\left|\lim_{m \to +\infty}f_n(x)-f_m(x)\right| \leq \epsilon, \quad\forall\,n \geq n_0,\quad\forall\,x \in X.$$Now, the pointwise limit exists, so we solve the limit inside $|\cdot|$: $$|f_n(x) - f(x)| \leq \epsilon, \quad \forall\,n\geq n_0,\quad \forall\,x \in X.$$After this, we can come back with $\sup_{x \in X}$, because of the $\forall\,x \in X$ bit. If the inequality were $<$, then it would become $\leq$ now. We have: $$\sup_{x \in X}|f_n(x)-f(x)|\leq \epsilon, \quad \forall\, n \geq n_0.$$But this last assertion is the definition of $f_n \to f$.