Preimage theorem

See Wikipedia. In some sense is a version of the Implicit Function Theorem.

Theorem
Let $f:M\to N$ a smooth map between manifolds, and let $y\in N$ be a regular value of $f$. Then $f^{-1}(y)$ is an embedded manifold of $M$.
$◼$

It is a corollary of the Constant rank level set theorem (see @lee2013smooth page 113):
Theorem
Let $M$ and $N$ be smooth manifolds and $F$ a smooth map between them, with constant rank $k$. Each level set of $F$ is a closed embedded manifold of codimension $k$ in $M$.
$◼$