Functional equation for tan If $f$ is a differentiable function on $\mathbb{R}$ and $f'(0)=2$ satisfying
$$f(x+y) = \frac{f(x)+f(y)}{1-f(x)f(y)},$$
then to prove that $f(x)=\tan 2x$.
I know that we must prove using the first definition(principle) of differentiation but I am not able to proceed. I got $f(0)=0$ and I also proved function is odd.
 A: As suggested by user marty cohen, I'll expand his hint into a full answer. We have:
$$\begin{array}
\nbsp f'(x) &=& \displaystyle\lim_{y\to 0} \dfrac{f(x+y)-f(x)}{y}\\
&=&\displaystyle\lim_{y\to 0} \dfrac{f(x)+f(y)-f(x)[1-f(x)f(y)]}{y[1-f(x)f(y)]}\\
&=&\displaystyle\lim_{y\to 0} \dfrac{f(y)+f(x)^2 f(y)}{y[1-f(x)f(y)]}\\
&=&\displaystyle\lim_{y\to 0} \left(\dfrac{f(y)}{y} \;\cdot \dfrac{1+f(x)^2}{1-f(x)f(y)}\right)\\
&=&f'(0) \cdot(1+f(x)^2)\\
&=&2(1+f(x)^2) 
\end{array}$$
where in the next-to-last line we use the definition of $f'(0)$, as well as continuity of $f$ and $f(0)=0$.
Now the differential equation 
$$y' = 2(1+y^2)$$
has the general solution $f(x)= \tan(2x+C)$; the condition $f(0) = 0$ forces $C=0$, so
$$f(x) = \tan(2x)$$
is the only possible solution for such an $f$. However, this $f$ is not defined at $x \in \lbrace \dfrac{k \pi}{2}: k \in \mathbb Z\rbrace$, so if one is formal and interprets "differentiable on $\mathbb R$" as "defined and differentiable on all of $\mathbb{R}$", the question as stated has no solution.
A: If a solution exists it has  to be $f(x)=\tan(2x)$, (not $2\tan\, x$). Let $g(x)=\tan^{-1}f(x)$. Then we get $g(x+y)=g(x)+g(y)$ which implies (by continuity) that $g(x)=cx$ for some $c$. Hence $f(x)=\tan (cx)$ and we can find $c$ from the fact that $f'(0)=2$.
As already pointed out $tan(2x)$ is not defined at certain points. This proves that there is no differentiable function on $\mathbb R$ satisfying the given equation
A: Find $(f(x+y)-f(x))/(y)$ and let
$y \to 0$.
Use $f(0)=0$.
