Tracking issue for differential geometry elaborators

#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 (#30879)

Basic differentiability elaborators

• for ContMDiff{WithinAt,At,On}
• for MDifferentiable{WithinAt,At,On}
• for mfderiv{Within}
• for HasMFDeriv{Within} (#30413)
• for UniqueDiffOn and UniqueDiffWithinAt (#40748) slightly different, because the model's type needs to be extracted from a set
• for tangentMap and tangentMapWithin (#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 (#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 #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 (#28032)
• infer a model with corners on the space H a manifold is modelled on (#28032)
• a space of continuous linear equivalences (#30413)
• a closed real interval (Set.Icc) (#30413)
• Euclidean half-space and friends (#30744)
• the complex upper half plane (#30413)
• units in a normed algebra (#30744)
• a metric sphere in a normed space (#30744)
• n-ary products, disjoint unions and open subsets (#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: #36230
• #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.