A nonzero complex derivative gives a local biholomorphism

By [L1], $\det Df(a)=\mathrm{\mid }{f}^{\mathrm{\prime }}(a){\mathrm{\mid }}^2>0$, so the real derivative $Df(a)$ is invertible.

Apply [L2] to the underlying smooth real map: there are open neighbourhoods $V_0$ of $a$ and $W_0$ of $f(a)$ such that $f{\mathrm{\mid }}_{V_0}:V_0\to W_0$ is bijective with a $C^1$ inverse $g$.

At every $w\in W_0$, the derivative $Df(g(w))$ is multiplication by $f^{\mathrm{\prime }}(g(w))$ by [L3], and it is invertible by the inverse-function construction. Hence $Dg(w)=Df(g(w){)}^{-1}$ is multiplication by $1\mathrm{/}{f}^{\mathrm{\prime }}(g(w))$; [L3] makes $g$ complex differentiable there with the displayed derivative.

Choose a disc $V$ centred at $a$ with closure contained in $V_0$, and put $W:=f[V]$. The disc $V$ is nonempty and open, and the triangle inequality keeps the segment between any two of its points inside it, so [L5] makes $V$ connected and hence a complex domain. The homeomorphism $f{\mathrm{\mid }}_{V_0}$ makes $W$ open, while [L4] makes it connected as the continuous image of $V$. Thus $V$ and $W$ are complex domains, and steps 2.1 and 3.1 show that $f{\mathrm{\mid }}_V$ and its inverse are holomorphic. Hence $f{\mathrm{\mid }}_V:V\to W$ is biholomorphic.