feat: custom elaborators for differential geometry (leanprover-community#27021)

Add two sets of custom elaborators for differential geometry, to
- infer the model with corners in `MDifferentiable{WithinAt,At,On}` or `ContMDiff{WithinAt,At,On}` expressions from the local context, and provide shorter notation in that setting
- do the same for mfderiv: `mfderiv% f` is shorthand for `mfderiv I J f`; `mfderiv[s] f x` is short for `mfderivWithin I J f s`
- convert a fibre bundle section from a dependent section to a function into the total space, making working with differentiability of sections of fibre bundles less cumbersome

This was [discussed on zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Differential.20geometry.20elaborators.20experiment/with/528035295), to overall broad consensus.

This code has substantial tests (which have caught bugs in the past). It has also been tested in the branch in leanprover-community#26221 (uncovering minor issues, but not substantial ones

Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
Co-authored-by: thorimur <thomasmurrills@gmail.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: 3 people

Mathlib.lean

@@ -3936,6 +3936,7 @@ import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
 import Mathlib.Geometry.Manifold.MFDeriv.Tangent
 import Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
 import Mathlib.Geometry.Manifold.Metrizable
+import Mathlib.Geometry.Manifold.Notation
 import Mathlib.Geometry.Manifold.PartitionOfUnity
 import Mathlib.Geometry.Manifold.PoincareConjecture
 import Mathlib.Geometry.Manifold.Riemannian.Basic