Implicit funtion theorem states that if (or nonsingular), then near we can uniquely solve from the equation . Moreover smoothness of determines smoothness of . Usually at least is .
A deep result is that in order to solve a continuous it’s enough that is everywhere differentiable (see Tao’s post), which reminds one an other deep result called invariance of domain (there is a similar result that we may call “invariance of Borel set”, see this SE post. But it does not require the same dimension).
Now let’s focus on . Assume that is defined implicitly (sometimes we intentionally make it implicit) by , differentiate the equation we get . Note that we are not losing much information because any solution stays in a level set of . But now which is a reasonable ODE with initial data .
For some problems this has given us a desired formula for :
Implict funtion theorem is substantially used in differentiable manifolds, method of characteristics for first order nonlinear PDE’s.
Implicit funtion theorem can even be generalized to infinite dimension, which is called Nash-Moser theorem. Literally, the proof implementes Nash-Moser iteration scheme.