Exercise on the implicit function theorem. 
Prove that the equation $x^2+y^2+\sin y=0$ defines a unique function $y=f(x)$ in a neighbourhood of $(0,0)$. Prove also that in $x=0$ there's a maxima for $f$.

I tried to do this exercise in two different ways and I'm asking you to tell me if I did something wrong, if the procedure is correct and if I could have done something better.
To prove that the equation defines a unique function $y=f(x)$ I want to use the implicit function theorem with the function $F(x,y)=x^2+y^2+\sin y$.
We have that $F(0,0)=0$ and $F$ is clearly $C^{\infty}$ so we don't have regularity problems. It's easy to verify that $F_y(x,y)=2y+\cos y$ and so $F_y(0,0)=1 \neq 0$.
For the implicit function theorem we have that there exists a unique function $f \colon \mathbb{R} \to \mathbb{R}$ at least defined in a neighbourhood of $0$ such that $y=f(x)$. We also remind that as $F$ is $C^{\infty}$ even $f$ is $C^{\infty}$.
Now we have the two different solutions for the second question, proving that in $x=0$ there is a maxima.


*

*We know from the implicit function theorem that 
$$f'(x)=-\frac{F_x(x,f(x))}{F_y(x,f(x))}$$
and so 
$$f'(x)=0$$
which tells us that $x=0$ is a stationary point for $f$. We can now use the chain rule to say that
$$f''(x)=-\frac{[F_{xx}(x,f(x))+F_{xy}(x,f(x))f'(x)]F_y(x,f(x))-F_x(x,f(x))[F_{yx}(x,f(x))+F_{yy}(x,f(x))}{F_y(x,f(x))^2}$$
from which $f''(0)<0$ and so $f$ has a maxima in $0$.

*We know that $f$ is $C^{\infty}$ so we have that
$$f(x)=f(0)+f'(0)x+\frac{f''(0)}{2}x^2+o(x^2)$$
and for what we observed in the first part we have $f(0)=f'(0)=0$. We know also that $F(x,f(x))=0$ and so, by plugging in the last equation the expression we found for $f(x)$ we have that 
$$x^2+\frac{f''(0)}{2}x^2+o(x^2)=0 \implies f''(0)=-2$$
and so the thesis.
Is it alright? Suggestions?

Your reasoning looks correct to me, and the first idea seems to work fine (I didn't check the details of your computation of the second derivative, though). 
I am a little subconscious about the second idea, since little o only makes sense "in the limit" as $x\rightarrow0$. I guess you can make it work, but you would have to be careful to make it rigorous. 
In the same spirit, however, I can suggest the following: you know that $f(0)=0$ and that
$$
F(x,f(x))=x^2+(f(x))^2+\sin (f(x))=0
$$
holds in a neighborhood of the origin, correct? In particular, close to $0$
$$
\sin (f(x))=-(x^2+(f(x))^2)<0
$$
so $f(x)$ has to be negative there (otherwise you would reach a contradiction). Therefore, $0$ is a local maximum.  Does that make sense?
