feat: improve doc-strings for differential geometry elaborators

[grunweg]

Right now, the custom elaborators in the manifold library have doc-strings which explain what the elaborator
expands to --- but don't show what the expanded concept means. It would be much better to show that also.
Verso allows doing so easily: this PR implements this as a proof of concept for the elaborator for mvfderiv.

This is not ready to land yet:

• the verso command defined currently works outside the module system, but not inside yet (this is because of a core bug fixed yesterday; it will be fixed in the next Lean release)

• the verso command should move to a better place (at least Geometry/Manifold/Notation.lean, perhaps even lower)

• Right now, the concatenated doc-string is formatted as pure text (not markdown): Lean core will implement this soon, but has not done so yet.

• this technique should be applied to all the custom elaborators

• the doc-strings of the elaborators may need to be rewritten, to start with the subject they're defining. (Once this happens, just concatenating the doc-strings produces reasonable results. This PR does this for mvfderiv only.)

Made with in-person help of David Thrane Christiansen at the MI retreat. Thanks a lot!

---

[github-actions]

PR summary c3f2e7b10d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.MFDeriv.NormedSpaceVersoPoC (new file)	2176

---

Declarations diff

+ Differentiable.comp_mdifferentiable
+ Differentiable.comp_mdifferentiableAt
+ Differentiable.comp_mdifferentiableWithinAt
+ DifferentiableAt.comp_mdifferentiableAt
+ DifferentiableAt.comp_mdifferentiableWithinAt
+ DifferentiableWithinAt.comp_mdifferentiableWithinAt
+ DifferentiableWithinAt.mdifferentiableWithinAt_of_comp_extChartAt_symm
+ HasMFDerivAt.smul
+ MDifferentiable.cle_arrowCongr
+ MDifferentiable.clm_apply
+ MDifferentiable.clm_comp
+ MDifferentiable.clm_postcomp
+ MDifferentiable.clm_precomp
+ MDifferentiable.clm_prodMap
+ MDifferentiable.smul
+ MDifferentiableAt.cle_arrowCongr
+ MDifferentiableAt.clm_apply
+ MDifferentiableAt.clm_comp
+ MDifferentiableAt.clm_postcomp
+ MDifferentiableAt.clm_precomp
+ MDifferentiableAt.clm_prodMap
+ MDifferentiableAt.smul
+ MDifferentiableOn.cle_arrowCongr
+ MDifferentiableOn.clm_apply
+ MDifferentiableOn.clm_comp
+ MDifferentiableOn.clm_postcomp
+ MDifferentiableOn.clm_precomp
+ MDifferentiableOn.clm_prodMap
+ MDifferentiableOn.smul
+ MDifferentiableWithinAt.cle_arrowCongr
+ MDifferentiableWithinAt.clm_apply
+ MDifferentiableWithinAt.clm_comp
+ MDifferentiableWithinAt.clm_postcomp
+ MDifferentiableWithinAt.clm_precomp
+ MDifferentiableWithinAt.clm_prodMap
+ MDifferentiableWithinAt.differentiableWithinAt_comp_extChartAt_symm
+ MDifferentiableWithinAt.smul
+ extDerivFun
+ fromTangentSpace_mfderiv_smul
+ fromTangentSpace_mfderiv_smul'
+ fromTangentSpace_mfderiv_smul_apply
+ fromTangentSpace_mfderiv_smul_apply'
+ mfderiv_smul
+ mvfderiv
++ foobar

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.