[Merged by Bors] - feat: more extensions for differential geometry elaborators by grunweg · Pull Request #30744 · leanprover-community/mathlib4

grunweg · 2025-10-21T09:20:06Z

Support inferring a model with corners in all remaining instances in mathlib, except for products and direct sums:

on Euclidean space, half-space or quadrants.
for the units in a normed algebra (including GL(V))
the unit interval
on the complex unit circle
on a metric sphere in a real or complex inner product space
also support finding a model on a domain which is an InnerProductSpace (hence only indirectly a normed space)

depends on: [Merged by Bors] - feat: further extensions of the differential geometry elaborators #30413
depends on: [Merged by Bors] - feat: beta reduce in the T% elaborator #30879
depends on: [Merged by Bors] - fix: example of GL(V) being a Lie group #33923 (a 5 line fix)

github-actions · 2025-10-21T09:21:19Z

PR summary 2b4c6152f1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ isCLMReduciblyDefeqCoefficients

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 script/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).

thorimur · 2025-10-27T18:14:54Z

By the way, does this depend on #30879, or is #30879 meant to split out the T% refactoring into a separate PR? (I suspect #30879 will get merged first anyway, so feel free to slap a dependence on this PR and avoid wrangling git if it's a hassle :) )

grunweg · 2025-10-27T19:33:19Z

Thanks for asking! I think I originally added the refactoring to this PR, and then decided that #30879 would also be a good place for it. Merging that one first should do the trick. I've added the dependency formally.

grunweg · 2025-10-27T19:33:46Z

(That might not make a big difference for reviewing: once #30413 is merged, I'll rebase this PR, and then hopefully commits are somewhat atomic, i.e. can be reviewed separately.)

grunweg · 2025-10-28T10:25:29Z

I have rebased this PR. I'll squash some of the intermediate commits about units of normed algebra next (as those are very not-atomic).

grunweg · 2025-10-28T12:46:27Z

I just squashed some intermediate commits: the history about inferring a sphere is still non-atomic, but most commits before it hopefully are. (I also made some progress on inferring a sphere, but the last piece of code still doesn't work. Help with that is welcome.)

mathlib4-merge-conflict-bot · 2025-11-19T08:16:30Z

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

This function needs a better name!

This code has not been changed in this PR, but let's add a test anyway. Any behaviour or diagnostics changes will come in a future PR.

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

grunweg · 2026-01-28T15:19:07Z

Thanks for the review!
bors merge

Support inferring a model with corners in all remaining instances in mathlib, except for products and direct sums: - on Euclidean space, half-space or quadrants. - for the units in a normed algebra (including GL(V)) - the unit interval - on the complex unit circle - on a metric sphere in a real or complex inner product space - also support finding a model on a domain which is an `InnerProductSpace` (hence only indirectly a normed space) Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-01-28T16:03:38Z

Build failed (retrying...):

Post-Build Step

mathlib-bors · 2026-01-28T16:23:50Z

Canceled.

grunweg · 2026-01-28T16:24:16Z

The test from the last commit failed the bors batch with diffs like

  -   ModelWithCorners.{u_1, ?u.235761, ?u.235762} 𝕜 ?E' ?H'
  +   ModelWithCorners.{u_1, ?u.235719, ?u.235720} 𝕜 ?E' ?H'

(It is fine on my computer, and even deterministic.) Ideas on writing a more robust test are welcome: in the mean-time, let's disable it so this PR can land.
bors r+

Support inferring a model with corners in all remaining instances in mathlib, except for products and direct sums: - on Euclidean space, half-space or quadrants. - for the units in a normed algebra (including GL(V)) - the unit interval - on the complex unit circle - on a metric sphere in a real or complex inner product space - also support finding a model on a domain which is an `InnerProductSpace` (hence only indirectly a normed space) Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-01-28T16:41:58Z

Pull request successfully merged into master.

Build succeeded:

set_option pp.mvars false normalises the universe levels, making the output sufficiently deterministic. Follow-up to leanprover-community#30744.

…tors (#34527) When a tracing option is already set, we don't need to tell the user about it. Follow-up to #30744.

`set_option pp.mvars false` normalises the universe levels, making the output sufficiently deterministic. Follow-up to #30744.

…er-community#30744) Support inferring a model with corners in all remaining instances in mathlib, except for products and direct sums: - on Euclidean space, half-space or quadrants. - for the units in a normed algebra (including GL(V)) - the unit interval - on the complex unit circle - on a metric sphere in a real or complex inner product space - also support finding a model on a domain which is an `InnerProductSpace` (hence only indirectly a normed space) Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

…tors (leanprover-community#34527) When a tracing option is already set, we don't need to tell the user about it. Follow-up to leanprover-community#30744.

…prover-community#34562) `set_option pp.mvars false` normalises the universe levels, making the output sufficiently deterministic. Follow-up to leanprover-community#30744.

…er-community#30744) Support inferring a model with corners in all remaining instances in mathlib, except for products and direct sums: - on Euclidean space, half-space or quadrants. - for the units in a normed algebra (including GL(V)) - the unit interval - on the complex unit circle - on a metric sphere in a real or complex inner product space - also support finding a model on a domain which is an `InnerProductSpace` (hence only indirectly a normed space) Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

…tors (leanprover-community#34527) When a tracing option is already set, we don't need to tell the user about it. Follow-up to leanprover-community#30744.

…prover-community#34562) `set_option pp.mvars false` normalises the universe levels, making the output sufficiently deterministic. Follow-up to leanprover-community#30744.

grunweg mentioned this pull request Oct 21, 2025

Tracking issue for differential geometry elaborators #30503

Open

26 tasks

github-actions bot added the t-differential-geometry Manifolds etc label Oct 21, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 21, 2025

grunweg force-pushed the diffgeo-custom-elaborators-evenmore branch 6 times, most recently from 102b492 to c99299a Compare October 25, 2025 09:54

grunweg mentioned this pull request Oct 25, 2025

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

Closed

3 tasks

thorimur self-assigned this Oct 27, 2025

grunweg added the t-meta Tactics, attributes or user commands label Oct 27, 2025

grunweg force-pushed the diffgeo-custom-elaborators-evenmore branch 2 times, most recently from 371d1ce to fe3335b Compare October 28, 2025 10:25

grunweg force-pushed the diffgeo-custom-elaborators-evenmore branch 2 times, most recently from 8225168 to 9edcbe6 Compare October 28, 2025 12:45

grunweg force-pushed the diffgeo-custom-elaborators-evenmore branch from bc045d4 to 9cb7b4f Compare November 12, 2025 22:31

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

grunweg force-pushed the diffgeo-custom-elaborators-evenmore branch from 711ca00 to ec30f7a Compare November 21, 2025 07:47

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 21, 2025

grunweg added 3 commits November 26, 2025 11:44

Support Euclidean half-space (with tests)

643cf57

Also support Euclidean space and Euclidean quadrants

fb212fa

chore: extract test for clms

85107f0

This function needs a better name!

grunweg and others added 4 commits January 28, 2026 16:00

chore: add a test for ContinuousLinearMaps over not the identity

83335b5

This code has not been changed in this PR, but let's add a test anyway. Any behaviour or diagnostics changes will come in a future PR.

Apply suggestion from @Vierkantor

a9f4213

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

[pre-commit.ci lite] apply automatic fixes

db013e4

Fix line length; update test output

0245629

ghost added the ready-to-merge This PR has been sent to bors. label Jan 28, 2026

grunweg mentioned this pull request Jan 28, 2026

[Merged by Bors] - chore: avoid redundant error message in differential geometry elaborators #34527

Closed

1 task

Disable brittle test

bbad99d

mathlib-bors bot changed the title ~~feat: more extensions for differential geometry elaborators~~ [Merged by Bors] - feat: more extensions for differential geometry elaborators Jan 28, 2026

mathlib-bors bot closed this Jan 28, 2026

grunweg deleted the diffgeo-custom-elaborators-evenmore branch January 28, 2026 16:46

grunweg mentioned this pull request Jan 29, 2026

[Merged by Bors] - chore: fix and re-enable differential geometry elaborators test #34562

Closed

mathlib-bors bot pushed a commit that referenced this pull request Jan 29, 2026

chore: avoid redundant error message in differential geometry elabora…

0d1bf8c

…tors (#34527) When a tracing option is already set, we don't need to tell the user about it. Follow-up to #30744.

mathlib-bors bot pushed a commit that referenced this pull request Jan 30, 2026

chore: fix and re-enable differential geometry elaborators test (#34562)

abd3b63

`set_option pp.mvars false` normalises the universe levels, making the output sufficiently deterministic. Follow-up to #30744.

mathlib-bors bot pushed a commit that referenced this pull request Jan 30, 2026

chore: fix and re-enable differential geometry elaborators test (#34562)

2b374df

`set_option pp.mvars false` normalises the universe levels, making the output sufficiently deterministic. Follow-up to #30744.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: more extensions for differential geometry elaborators#30744

[Merged by Bors] - feat: more extensions for differential geometry elaborators#30744
grunweg wants to merge 38 commits intoleanprover-community:masterfrom
grunweg:diffgeo-custom-elaborators-evenmore

grunweg commented Oct 21, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Oct 21, 2025 •

edited

Loading

Uh oh!

thorimur commented Oct 27, 2025 •

edited

Loading

Uh oh!

grunweg commented Oct 27, 2025

Uh oh!

grunweg commented Oct 27, 2025

Uh oh!

grunweg commented Oct 28, 2025 •

edited

Loading

Uh oh!

grunweg commented Oct 28, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

grunweg commented Jan 28, 2026

Uh oh!

mathlib-bors bot commented Jan 28, 2026

Uh oh!

mathlib-bors bot commented Jan 28, 2026

Uh oh!

grunweg commented Jan 28, 2026 •

edited

Loading

Uh oh!

mathlib-bors bot commented Jan 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

grunweg commented Oct 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2b4c6152f1

Import changes for modified files

Declarations diff

Uh oh!

thorimur commented Oct 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg commented Oct 27, 2025

Uh oh!

grunweg commented Oct 27, 2025

Uh oh!

grunweg commented Oct 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg commented Oct 28, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

grunweg commented Jan 28, 2026

Uh oh!

mathlib-bors bot commented Jan 28, 2026

Uh oh!

mathlib-bors bot commented Jan 28, 2026

Uh oh!

grunweg commented Jan 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-bors bot commented Jan 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

grunweg commented Oct 21, 2025 •

edited

Loading

github-actions bot commented Oct 21, 2025 •

edited

Loading

thorimur commented Oct 27, 2025 •

edited

Loading

grunweg commented Oct 28, 2025 •

edited

Loading

grunweg commented Jan 28, 2026 •

edited

Loading