[Merged by Bors] - feat: support products and disjoint unions in the differential geometry elaborators

[grunweg]

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.

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.

---

• depends on: [Merged by Bors] - fix: check for a space of continuous linear maps over not-the-identity #35176
• depends on: [Merged by Bors] - feat: more extensions for differential geometry elaborators #30744
• depends on: [Merged by Bors] - feat: beta reduce in the T% elaborator #30879

[grunweg]

Next step: update the golfing PR to also incorporate this one, try golfing the heck out of mathlib and re-benchmark.

[github-actions]

PR summary 2d973f3355

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ FindModelResult
+ NormedSpaceInfo
+ findModelInner
+ instance : Coe Expr FindModelResult
- findModel

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[grunweg]

I have just updated this work on top of the current state in #30744 (which is now maintainer merged, hence will hopefully land soon). #30421 contains the current code; I will overwrite this branch accordingly once this PR is unblocked.

[thorimur]

Let me add one bundle of review suggestions + questions for now, all centered on isCLMReducibleDefeqCoefficients:

• isCLMReducibleDefeqCoefficients, returning three Exprs, is riiiight on the edge of needing a structure return type, I feel! :) I've marked it private for now, seeing as it only has two usages.
• I think it can return the Exprs instead of wrapping this in an Option, as in both of its uses, we throw approximately the same error (up to the word "either"). Are there cases you anticipate that make the Option useful?
• I changed indentation, and used pureIsDefEq instead of isDefEq to avoid assigning mvars.
• I added a check that the map was a RingHom.id, seeing as that was a TODO. Are there cases that make this more complicated? (Coercions or such?) Feel free to revert this change if so (and just leave a quick comment explaining why it's a todo/what the blocking issue is :) )

Please take the commit here as a companion to the comment showing the discussed changes, rather than a final version of the code :)

[thorimur]

I think this is really close. :) I wanted to give you some more review comments to act on immediately if helpful.

[grunweg]

Let me add one bundle of review suggestions + questions for now, all centered on isCLMReducibleDefeqCoefficients:

* `isCLMReducibleDefeqCoefficients`, returning three `Expr`s, is riiiight on the edge of needing a structure return type, I feel! :) I've marked it `private` for now, seeing as it only has two usages.

* I think it can return the `Expr`s instead of wrapping this in an `Option`, as in both of its uses, we throw approximately the same error (up to the word "either"). Are there cases you anticipate that make the `Option` useful?

* I changed indentation, and used `pureIsDefEq` instead of `isDefEq` to avoid assigning mvars.

* I added a check that the map was a `RingHom.id`, seeing as that was a TODO. Are there cases that make this more complicated? (Coercions or such?) Feel free to revert this change if so (and just leave a quick comment explaining why it's a todo/what the blocking issue is :) )

Please take the commit here as a companion to the comment showing the discussed changes, rather than a final version of the code :)

Thanks a lot for the review (as usual). There is actually #35176, which addresses the exact same TODO :-)
Actually, how about I roll your changes into that PR, you take a quick look if you like them, and then we get that PR in first?

[thorimur]

Sounds good (re: rolling changes into that PR)! :)

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - fix: check for a space of continuous linear maps over not-the-identity #35176
• [Merged by Bors] - feat: more extensions for differential geometry elaborators #30744
• [Merged by Bors] - feat: beta reduce in the T% elaborator #30879
  By Dependent Issues (🤖). Happy coding!

[thorimur]

Looks good to me after these changes! :) (And after the TODO in the last commit!)

[grunweg]

Thanks for your comments again - all addressed.

[thorimur]

Wonderful! Looking forward to this finally being merged! :)

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by thorimur.

[ocfnash]

Thank you both!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step