[Merged by Bors] - chore: rename declarations whose names do not match their statements by Multramate · Pull Request #44051 · leanprover-community/mathlib4

Multramate · 2026-09-21T15:28:59Z

The lemmas about IsLocalDiffeomorphAt.localInverse simply were in the wrong order: they should say continuous_localInverse etc. instead of localInverse_continuous. In some cases, both variants already existed (so we deprecated the wrongly named one).

Split out of #43889.

Written with the assistance of Claude (Claude Code).

Unlike the other parts of the split, these old names are well-formed and pronounceable — there is no misspelling to spot. They simply say the wrong thing, so each one needs its statement read.

coeff_isPWOsupport → isPWO_support_coeff — the conclusion really is IsPWO (support (coeff ..))
preserveFiniteLimits_plusFunctor → preservesFiniteLimits_plusFunctor — the verb tracks the head symbol PreservesFiniteLimits
tendsto_of_uncrossing_lt_top → tendsto_of_upcrossings_lt_top — wrong word and wrong number, checked against the hypothesis upcrossings a b f w
substr_num_den' → sub_num_den'
nneg_mul_add_sq_of_abs_le_one → nonneg_mul_add_sq_of_abs_le_one

lemmas

contmdiffOn_localInverse → contMDiffOn_localInverse, and for consistency the two lemmas below it take the same order: localInverse_contMDiffAt → contMDiffAt_localInverse and localInverse_mdifferentiableAt → mdifferentiableAt_localInverse. All three old names are deprecated and their use sites updated.

localInverse_contMDiffOn already existed further down the file with a byte-identical statement and proof. The duplicate is dropped and the lemma moved above its first use, so that name is deprecated to contMDiffOn_localInverse too.

The review suggested mdifferentiableAt_contMDiffAt for the third of these. Its statement is MDiffAt hf.localInverse (f x) — about the local inverse, not about contMDiffAt — so mdifferentiableAt_localInverse is used instead, matching the other two. Happy to change it if the original was meant literally.

Notes on the review

preserveFiniteLimits_plusFunctor gets no deprecated alias: it is an instance, so it is found by typeclass resolution rather than by name, and nothing in Mathlib refers to it by name.

sub_num_den' is left as proposed. The statement is (q - r).num * q.den * r.den = (q.num * r.den - r.num * q.den) * (q - r).den, which is genuinely subtraction; it sits directly below add_num_den' and mul_num_den' and its proof goes via add_num_den' and sub_eq_add_neg; and no sub_num_den or sub_num_den' exists anywhere else in Mathlib or the toolchain, so there is no collision.

(see #44049, #44050 and #44052 for the other parts).

These old names are well-formed and pronounceable - there is no misspelling to spot - they simply say the wrong thing, so each one needs the statement read. That is fine for six and intolerable interleaved with fifty others, which is why they are split out of leanprover-community#43889. - `coeff_isPWOsupport` -> `isPWO_support_coeff`: the conclusion really is `IsPWO (support (coeff ..))`. - `contmdiffOn_localInverse` -> `localInverse_contMDiffOn`. - `preserveFiniteLimits_plusFunctor` -> `preservesFiniteLimits_plusFunctor`: the verb tracks the head symbol `PreservesFiniteLimits`. - `tendsto_of_uncrossing_lt_top` -> `tendsto_of_upcrossings_lt_top`: wrong word and wrong number, checked against the hypothesis `upcrossings a b f w`. - `substr_num_den'` -> `sub_num_den'`: the statement is subtraction, and the new name matches the neighbouring `add_num_den'`. - `nneg_mul_add_sq_of_abs_le_one` -> `nonneg_mul_add_sq_of_abs_le_one`. `localInverse_contMDiffOn` already existed further down `Mathlib/Geometry/Manifold/LocalDiffeomorph.lean` with a byte-identical statement and proof; this moves the lemma above its first use and drops the duplicate, so the rename can take the name.

github-actions · 2026-09-21T15:30:16Z

PR summary 8083eb1ba6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ contMDiffAt_localInverse
+ contMDiffOn_localInverse
+ isPWO_support_coeff
+ mdifferentiableAt_localInverse
+ nonneg_mul_add_sq_of_abs_le_one
+ preservesFiniteLimits_plusFunctor
+ sub_num_den'
+ tendsto_of_upcrossings_lt_top
- preserveFiniteLimits_plusFunctor

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- unavailable)

⚠️ No declarations diff yet: there is no built master snapshot at this PR's merge-base (typically a bors-batch intermediate that CI never built). Merge master into this PR and push to refresh.

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 8083eb1ba6
Reference commit 4abb71fee8

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

grunweg

Thanks! A few minor comments. Please also update the PR description accordingly.

grunweg · 2026-09-21T15:38:52Z

  rw [← divInt_eq_div]

-theorem substr_num_den' (q r : ℚ) :
+theorem sub_num_den' (q r : ℚ) :


Let me flag this for a second pair of eyes.

I think this is fine? It's literally subtraction (apparently spelt substraction here for whatever reason), and there are already add_num_den and mul_num_den, etc.

- Drop the deprecated alias for `preserveFiniteLimits_plusFunctor`. It is an instance, so it is found by typeclass resolution rather than by name, and nothing in Mathlib refers to it by name. - Use `contMDiffOn_localInverse` rather than `localInverse_contMDiffOn`, as requested. `localInverse_contMDiffOn` exists on master, so it is deprecated to the new name alongside the misspelled `contmdiffOn_localInverse`. - Follow the same order for the two neighbouring lemmas: `localInverse_contMDiffAt` -> `contMDiffAt_localInverse` and `localInverse_mdifferentiableAt` -> `mdifferentiableAt_localInverse`, both deprecated, with their use sites updated. The review suggested `mdifferentiableAt_contMDiffAt` for the last of these, but the statement is `MDiffAt hf.localInverse (f x)` - about the local inverse, not about `contMDiffAt` - so `mdifferentiableAt_localInverse` is used instead, matching the other two. `sub_num_den'` is left as is: the statement is subtraction, it sits directly below `add_num_den'` and `mul_num_den'`, its proof goes via `add_num_den'`, and no `sub_num_den`/`sub_num_den'` exists anywhere else.

The previous run failed in `Test and lint` because the prebuilt artifact download returned 403, so `lake lint` rebuilt Mathlib from source and hit the 10-minute timeout twice. No linter finding was reported. Empty commit to get a clean run.

grunweg · 2026-09-21T18:27:30Z

Thanks! I have drastically shortened the PR description. (Can you take that into account for the next PRs, please?) With that fixed, I think this PR is good to go.
bors merge

…44051) The lemmas about `IsLocalDiffeomorphAt.localInverse` simply were in the wrong order: they should say `continuous_localInverse` etc. instead of `localInverse_continuous`. In some cases, both variants already existed (so we deprecated the wrongly named one). Split out of #43889. Written with the assistance of Claude (Claude Code).

mathlib-bors · 2026-09-21T20:23:05Z

Pull request successfully merged into master.

Build succeeded:

…eanprover-community#44051) The lemmas about `IsLocalDiffeomorphAt.localInverse` simply were in the wrong order: they should say `continuous_localInverse` etc. instead of `localInverse_continuous`. In some cases, both variants already existed (so we deprecated the wrongly named one). Split out of leanprover-community#43889. Written with the assistance of Claude (Claude Code).

Multramate mentioned this pull request Sep 21, 2026

[Merged by Bors] - chore: fix instance and to_additive declaration names #44052

Closed

Multramate added easy < 20s of review time. See the lifecycle page for guidelines. LLM-generated PRs with substantial input from LLMs - review accordingly labels Sep 21, 2026

grunweg reviewed Sep 21, 2026

View reviewed changes

grunweg added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 21, 2026

Multramate removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 21, 2026

chore: retrigger CI

8083eb1

The previous run failed in `Test and lint` because the prebuilt artifact download returned 403, so `lake lint` rebuilt Mathlib from source and hit the 10-minute timeout twice. No linter finding was reported. Empty commit to get a clean run.

grunweg removed the easy < 20s of review time. See the lifecycle page for guidelines. label Sep 21, 2026

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Sep 21, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Sep 21, 2026

mathlib-bors Bot changed the title ~~chore: rename declarations whose names do not match their statements~~ [Merged by Bors] - chore: rename declarations whose names do not match their statements Sep 21, 2026

mathlib-bors Bot closed this Sep 21, 2026

Multramate mentioned this pull request Sep 22, 2026

chore: fix misspellings in declaration names #44049

Open

Navigation Menu

[Merged by Bors] - chore: rename declarations whose names do not match their statements - #44051

[Merged by Bors] - chore: rename declarations whose names do not match their statements#44051
Multramate wants to merge 3 commits into
leanprover-community:masterfrom
Multramate:split/typo-name-statement

Multramate commented Sep 21, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Sep 21, 2026 •

edited

Loading

Declarations diff (regex)

Uh oh!

grunweg left a comment

Uh oh!

Uh oh!

grunweg Sep 21, 2026

Uh oh!

Multramate Sep 21, 2026

Uh oh!

Uh oh!

Uh oh!

grunweg commented Sep 21, 2026

Uh oh!

mathlib-bors Bot commented Sep 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

Multramate commented Sep 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

lemmas

Notes on the review

Uh oh!

github-actions Bot commented Sep 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8083eb1ba6

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- unavailable)

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

grunweg Sep 21, 2026

Choose a reason for hiding this comment

Uh oh!

Multramate Sep 21, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

grunweg commented Sep 21, 2026

Uh oh!

mathlib-bors Bot commented Sep 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Multramate commented Sep 21, 2026 •

edited

Loading

github-actions Bot commented Sep 21, 2026 •

edited

Loading