#27021 added a first version of custom elaborators in differential geometry for reducing boilerplate and verbosity. This PR tracks missing features for them.

For the T% elaborators (which expands to TotalSpace.mk' calls):

• take any number or arguments, and beta_reduce them ([Merged by Bors] - feat: beta reduce in the T% elaborator #30879)

Basic differentiability elaborators

• for ContMDiff{WithinAt,At,On}
• for MDifferentiable{WithinAt,At,On}
• for mfderiv{Within}
• for HasMFDeriv{Within} ([Merged by Bors] - feat: further extensions of the differential geometry elaborators #30413)
• for UniqueDiffOn and UniqueDiffWithinAt --- slightly different, because the model's type needs to be extracted from a set
• for tangentMap and tangentMapWithin (feat: custom elaborators for TangentSpace and tangentMap(Within) #36155)
• any other constructions which mention a model with corners? Immersions, submersions and embeddings (in WIP PRs)?

General aspects of all differentiability elaborators

• support coercions ([Merged by Bors] - feat: support coercions in the differential geometry elaborators #30307)
• better errors in the CMDiff elaborator if n is simply forgotten (right now, this is just a parse error)
• helpful trace nodes, including better nesting
• more newcomer-friendly error messages: suggest the expanded form of the syntax, with any found models filled in. Perhaps suggest missing cases in these elaborators (when appropriate).
• diagnose why the IsImmersionAt elaborators fail in a different namespace: see feat: add custom elaborators for immersions #30504
• what's their desired scope: can they be made to assume no imports, and be imported and used in literally the files defining their concepts? or perhaps, not in those but all files depending on them? (that could be nice, never having to wonder about that)

Infer the model with corners in all currently known cases

• infer a model with corners on a TangentBundle ([Merged by Bors] - feat: miscellaneous improvements to the differential geometry elaborators #28032)
• infer a model with corners on the space H a manifold is modelled on ([Merged by Bors] - feat: miscellaneous improvements to the differential geometry elaborators #28032)
• a space of continuous linear equivalences ([Merged by Bors] - feat: further extensions of the differential geometry elaborators #30413)
• a closed real interval (Set.Icc) ([Merged by Bors] - feat: further extensions of the differential geometry elaborators #30413)
• Euclidean half-space and friends ([Merged by Bors] - feat: more extensions for differential geometry elaborators #30744)
• the complex upper half plane ([Merged by Bors] - feat: further extensions of the differential geometry elaborators #30413)
• units in a normed algebra ([Merged by Bors] - feat: more extensions for differential geometry elaborators #30744)
• a metric sphere in a normed space ([Merged by Bors] - feat: more extensions for differential geometry elaborators #30744)
• n-ary products, disjoint unions and open subsets ([Merged by Bors] - feat: support products and disjoint unions in the differential geometry elaborators #30463)

#30357 contains all or many of the current in-flight changes, and golfs as much of mathlib as possible using them.
Inspecting the remaining unsolved cases closely could turn up further bugs or missing features.

Add corresponding delaborators

• initial PR: [Merged by Bors] - feat: some delaborators for differential geometry #36230
• [Merged by Bors] - feat: delaborators for MDifferentiable(On) #36318
• remaining delaborators to come soon

Evolution mode, transforming the library

• allow adding a new elaborator/inferring a new model by writing some short meta code/using an attribute or so in the file defining the instance. This requires using an environment extension (but could make working with this much nicer; a downstream project could define a new instance, but also support finding the model).
• can we get rid of having to write elaborators for each new definition? speculative idea: could there be a tactic find_model M, and then for any definition requiring a model, make that parameter I := by find_model M?
• extend fun_prop to ContMDiff, and use find_model to power finding the model with corners for intermediate manifolds.

Some of these will be part of @scholzhannah's master's thesis --- talk to me if you would like to work on this, so we can avoid doing things twice.