There's this theorem in Spivak's book of Calculus:
Theorem 7
Suppose that $f$ is continuous at $a$, and that $f'(x)$ exists for all $x$ in some interval containing $a$, except perhaps for $x=a$. Suppose, moreover, that $\lim_{x \to a} f'(x)$ exists. Then $f'(a)$ also exists, and $$f'(a) = \lim_{x \to a} f'(x)$$
Proof
By definition, $$f'(a) = \lim_{h \to 0} \frac{f(a+h)-f(a)}{h}$$ For sufficiently small $h>0$ the function $f$ will be continuous on $[a,a+h]$ and differentiable on $(a,a+h)$ (a similar assertion holds for sufficiently small $h<0$). By the Mean Value Theorem there is a number $\alpha_h$ in $(a,a+h)$ such that $$\frac{f(a+h)-f(a)}{h} = f'(\alpha_h)$$ Now $\alpha_h$ approaches $a$ as $h$ approaches $0$, because $\alpha_h$ is in $(a,a+h)$; since $\lim_{x \to a} f'(x)$ exists, it follows that $$f'(a) = \lim_{h \to 0} \frac{f(a+h)-f(a)}{h} = \lim_{h \to 0} f'(\alpha_h) = \lim_{x \to a} f'(x)$$ (It is a good idea to supply a rigorous $\epsilon$-$\delta$ argument for this final step, which we have treated somewhat informally.) $\blacksquare$
Following the recommendation of supplying the details I had the question of $\alpha_h$ being a choice function. This is because for every $h$ there is the possibility of having a lot of points $c$ such that $f'(c)=\frac{f(a+h)-f(a)}{h}$. Then we choose one of them to have a function $\alpha_h$. I'm not sure though because I'm always struggling with the axiom of choice that I cannot distinguish if it's needed or not. Also maybe in this case what the author is saying is something different. Can you guys please help me?
Yes, this is an interesting technical point that is often overlooked. As written, Spivak is postulating the existence of the function that to each (positive, sufficiently small) $h$ assigns the value $\alpha_h$. On the face of it, this is an application of the axiom of choice, because the set of numbers $\tau$ between $a$ and $a+h$ such that $\displaystyle \frac{f(a+h)-f(a)}h=f'(\tau)$ does not need to be a singleton, or open, or closed, or any reasonably shaped set, so the problem of assigning to each such $h$ a specific such number $\tau$ requires infinitely many choices in what does not appear to be a straightforward definable manner.
One technical remark is that, using techniques of descriptive set theory, we can eliminate this use of choice since for $\eta>0$ small enough, the relation $$\{(h,\tau):0<|h|<\eta\mbox{ and }\frac{f(a+h)-f(a)}h=f'(\tau)\}$$ is Borel, and therefore admits what we call a co-analytic uniformization, provably in Zermelo-Fraenkel set theory without the axiom of choice. (This means that we can actually prove, without choice, the existence of a function $a_h$ as in Spivak's argument.)
That said, both this statement and its proof are definitely beyond the level of Spivak's textbook. Fortunately, in order to formalize what he does, we can proceed in a more elementary manner:
Let $L=\lim_{x\to a}f'(x)$, the limit whose existence is granted by assumption. For any $\epsilon>0$ there is a $\delta>0$ such that for any $\tau$, if $0\ne \tau$ and $|\tau|<\delta$, then $|f'(a+\tau)-L|<\epsilon$. It is enough to prove that $$ \left|\frac{f(a+h)-f(a)}h - L\right|<\epsilon $$ for any $h$ with $0\ne h$ and $|h|<\delta$. Since $\epsilon$ is arbitrary, this indeed shows that $f'(a)$ exists and equals $L$.
Now, given such an $h$, we know that there is a $\rho$ in the open interval with endpoints $a$ and $a+h$ such that $\displaystyle \frac{f(a+h)-f(a)}h=f'(\rho)$. There may in fact be many possible choices for $\rho$, but we do not need to choose any (that is, we do not need to assert the existence of the function $a_h$). Simply note that for any such $\rho$, we have $0<|\rho-a|<\delta$, and so indeed $$ \left|\frac{f(a+h)-f(a)}h - L\right|<\epsilon, $$ as needed.
A similar issue appears in (advanced) analysis, in the theory of the derivative, when studying Neugebauer's theorem that characterizes when a function is a derivative in terms of properties of a companion function playing the role of $a_h$ above. Without appealing to the descriptive set theoretic result mentioned above, Neugebauer's theorem appears to need more choice than the standard fragment usually assumed in analysis (dependent choices). I have not found any texts dealing with Neugebauer's theorem that address (or even appear aware of) this technicality.