The example of the implicit formula of the unit circle $x^2 + y^2 =1$ to set up the idea that in the neighborhood of points $(-1,0)$ and $(1,0)$ the explicit formula $y = \sqrt{1-x^2}$ (or, alternatively, $y=-\sqrt{1-x^2}$) breaks down, and to introduce the implicit function theorem, is quite intuitive: as much as at around $x=0$ the top (and bottom) of the circle in the explicit function are well defined, the problems around $(1,0)$ can be simply circumvented by flipping $x$ and $y$, and using $y$ now as free variable (looking at the circle "sideways" as it were).
However, I haven't seen the example of the circle spelled out to the last moving part of the theorem, and I wonder if it is because there are no more insights to be gleaned, due to the fact that the $f$ function in the theorem can be made explicit.
I imagine that going through the exercise would entail the following steps:
- Setting up $F(x,y)=x^2 + y^2 -1$, which is a $C^1$ function.
- The $(x_0,y_0)$ point in question could be $(1,0)$, which fulfills the condition of being in the level set for which $F(x,y)=0$ (i.e. the first condition).
- The second condition would entail realizing that $\frac{\partial F}{\partial y}=0$, but that, critically, $\frac{\partial F}{\partial x}=2x=2$.
The theorem now assures us that there is an implicit equation $x = f(y)$, which in this case would be $x=\sqrt{1-y^2}$, but it could not be found based on the theorem in general. And that this equation fulfills:
(i) $f(y_0) = x_0$, i.e $f(0)=1$
(ii) $F(f(y),y)=0$ for all $y$ in the neighborhood of (1,0).
(iii) $f'(y)=\frac{-\frac{\partial F}{\partial y}}{\frac{\partial F}{\partial x}}$. From line $(3)$ above we already know that this is $0$, and knowing $f$ in explicit form, we can also calculate $\frac{d}{dy}\,\sqrt{1-y^2}=\frac{-y}{\sqrt{1-y^2}}$, which evaluated at $(1,0)$ is zero.