I just had a student come to my office hours and ask me a ton of questions, the answer to all of which was "that's a slight variant to the implicit function theorem, which is proved by formal manipulation from the implicit function theorem". For example:
$\def\RR{\mathbb{R}}$ Let $f : \RR^n \to \RR$ be a smooth function and suppose that $\partial f/ \partial x_n \neq 0$. Then, locally, $(x_1, x_2, \ldots, x_{n-1}, f)$ are coordinates on $\RR^n$.
Let $f : \RR^n \to \RR$ be a smooth function and suppose that $\partial f/ \partial x_n \neq 0$. Then, locally, $(x_1, x_2, \ldots, x_{n-1})$ are coordinates on $\{ f=0 \}$.
Let $U$ be a small open set in $\RR^d$ and let $(f_1, \ldots, f_d): U \to \RR^n$ parameterize a patch on a manifold $M$ in $\RR^n$. Suppose that $\det (\partial f_i/\partial x_j)_{1 \leq i,j \leq d} \neq 0$. Then $x_1$, ..., $x_d$ are local coordinates on $M$.
Let $g_1$, ..., $g_{n-d}$ be smooth functions $\RR^n \to \RR$. Let $M= \{g_1=g_2=\ldots=g_{n-d} = 0 \}$. Suppose that $\det (\partial f_i/\partial x_j)_{1 \leq i,j \leq n-d} \neq 0$. Then $M$ is a smooth manifold of dimension $d$ and $x_{n-d+1}$, ..., $x_n$ are local coordinates near $0$.
Does anyone know a book which works through these sort of variants systematically?
I should mention that I actually need these facts for holomorphic functions. But I have a good reference for the holomorphic implicit function theorem: Gunning and Rossi, Chapter 1. The problem is that I want a reference which goes slowly through these variants, rather than assuming they are obvious corollaries.