feat: support products and disjoint unions in the differential geometry elaborators (#30463)

Add support for inferring a model with corners on
- products of manifolds
- disjoint unions of manifolds
- an open subset of a manifold

Note that these can be nested (e.g., a product with multiple factors, a disjoint union of four manifolds or combinations of these).

For binary products of normed spaces, we intentionally refuse to infer a model with corners, as there are two different possible options which are propositionally, but not definitionally equal. For now, we emit a warning to this effect instead. A future PR may remove it (and infer one of these variants): see [zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Differential.20geometry.20elaborators.20experiment/near/544942546).

This PR completes an important milestone: models with corners are now inferred for *all* instances mathlib knows about! Update the module doc-string accordingly.
A future PR will golf mathlib using these elaborators.

Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
Co-authored-by: thorimur <thomasmurrills@gmail.com>

Author: grunweg