feat(analysis/calculus/implicit): Implicit function theorem (#2749)
Fixes #1849
[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/2749.20Implicit.20function.20theorem).
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>