If you go a little bit further than the inverse and implicit function theorems, you can get a fairly practical theorem. <a href="https://en.wikipedia.org/wiki/Kantorovich_theorem">Kantorovich's theorem</a> gives you fairly strong sufficient conditions for a system of smooth equations to have a solution. Moreover it tells you how quickly Newton's method converges in that situation. For example, this theorem is used by <a href="https://arxiv.org/abs/0809.1203">Harriet Moser</a> to prove that <a href="https://en.wikipedia.org/wiki/SnapPea">SnapPea</a> does give approximations to <i>actual solutions</i> to the hyperbolic gluing equations. The applications of course are pretty broad, this is one on the fairly pure end of the spectrum. Kantorovich was an economist although I do not understand the economics problems he was interested in. If you're interested, this perspective on the inverse and implicit function theorems is in "full glory" in <a href="http://matrixeditions.com/UnifiedApproach4th.html">Hubbard's multi-variable calculus text</a>. 2nd answer: The proof of Sard's theorem is a delicate dance with the Implicit Function Theorem, Taylor's Theorem and some basic argument with Lebesgue measure zero.