feat: add and use custom (d)elaborators for mvfderiv, add basic API lemmas

[grunweg]

Add a custom elaborator (scoped to the Manifold namespace) shortening mvfderiv I f to d% f,
and have a corresponding delaborator also. Their implementation is fully analogous to the existing elaborators.

Also, rewrite Lie bracket lemmas to use mvfderiv instead of open-coding it.

Part of #36036, i.e. from the path towards the Levi-Civita connection and Riemanian curvature.
Related to fixing defeq abuses related to tangent space and scalar multiplication in mathlib.

Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com
Co-authored-by: Patrick Massot patrickmassot@free.fr

---

[grunweg]

This code was virtually all written by Patrick; I just made minor clean-ups (such as updating the module doc-string, or switching the notation to d% as discussed with Patrick and Heather). Before my clean-ups, I would have been happy to merge this PR directly. Given this, let's have another pair of eyes for good measure:
maintainer merge?

[github-actions]

PR summary c481c5c698

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ mvfderiv_const
+ mvfderiv_mul
+ mvfderiv_neg
+ mvfderiv_smul
+ mvfderiv_sub
- extDerivFun
- extDerivFun_add
- extDerivFun_zero

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.