[Merged by Bors] - chore: rename `mul_le_mul_right'` to `mul_le_mul_left` by YaelDillies · Pull Request #30242 · leanprover-community/mathlib4

YaelDillies · 2025-10-05T14:23:16Z

depends on: [Merged by Bors] - chore: use grw, gcongr more #30508
depends on: [Merged by Bors] - chore: use grw, gcongr even more #30632

github-actions · 2025-10-05T14:24:25Z

PR summary cf85478f35

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ LinearOrderedCommGroup.mul_lt_mul_right'
+ OrderedAddCommGroup.add_lt_add_left'
+ add_lt_add_left
+ mul_le_mul_iff_left
+ mul_le_mul_iff_right
+ mul_lt_mul_iff_left
+ mul_lt_mul_iff_right
+ nmul_le_nmul
+-+ add_le_add_left
+-- mul_lt_mul_left'
+-- mul_lt_mul_right'
+--+ mul_le_mul_left
+--+ mul_le_mul_right
- add_le_add_right
- add_lt_add_right
- mul_le_mul_left'
- mul_le_mul_right'
-+-+ mul_lt_mul_right
-+-+-+ isOrderedAddMonoid
--++ mul_lt_mul_left

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

scripts/nolints_prime_decls.txt

JovanGerb · 2025-10-10T15:13:47Z

Why don't you use grw to clean up the proofs?

YaelDillies · 2025-10-10T15:27:01Z

I like using calc + gcongr, because it makes the proofs more readable and maintainable, but I am indeed on the lookout for places where grw would be more readable.

mathlib4-merge-conflict-bot · 2025-10-13T03:41:14Z

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

Golf many proofs using `grw`, `gcongr`, `cutsat`, `linarith`... For this, tag a few more lemmas with `gcongr`, and make some existing ones stronger. The goal here is not necessarily to golf (although it usually is the case), but instead to reduce the number of explicit mentions of lemmas, as these are a maintainability concern. The precise golfs that are performed are motivated by leanprover-community#30242, where four pairs of very basic and widespread lemmas get swapped.

mathlib4-merge-conflict-bot · 2025-10-15T16:16:04Z

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

Golf many proofs using `grw`, `gcongr`, `cutsat`, `linarith`... For this, tag a few more lemmas with `gcongr`, and make some existing ones stronger. The goal here is not necessarily to golf (although it usually is the case), but instead to reduce the number of explicit mentions of lemmas, as these are a maintainability concern. The precise golfs that are performed are motivated by #30242, where four pairs of very basic and widespread lemmas get swapped. The best way to reduce the number of swaps needed is to simply not mention the lemmas explicitly.

Vierkantor

bors d=@JovanGerb

mathlib-bors · 2025-11-20T17:09:38Z

✌️ JovanGerb can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

JovanGerb

I think a ton of these proofs can be golfed with grw, but that need not be done by this PR.

LGTM, just a few comments

JovanGerb · 2025-11-20T23:03:44Z

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

+    IsOrderedAddMonoid (WithZero α) := by
+  have := WithZero.addLeftMono zero_le
+  exact ⟨fun _ _ ↦ add_le_add_left, by simpa [add_comm] using fun _ _ ↦ add_le_add_left⟩


Why did this get longer?

because IsOrderedAddMonoid.mk automatically proves one field from the other, but WithZero.addLeftMono zero_le now proves the other (instead of previously the one)

Mathlib/Algebra/Order/ToIntervalMod.lean

Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

JovanGerb · 2025-11-20T23:26:01Z

Mathlib/Data/ENNReal/Action.lean


 instance : SMulPosMono ℝ≥0 ℝ≥0∞ where
-  smul_le_smul_of_nonneg_right _r _ _a _b hab := mul_le_mul_right' (coe_le_coe.2 hab) _
+  smul_le_smul_of_nonneg_right _r _ _a _b hab := _root_.mul_le_mul_left (coe_le_coe.2 hab) _


Why did this become _root_.? (same below)

because ENNReal.mul_le_mul_left isn't protected

YaelDillies · 2025-11-21T09:31:16Z

I think a ton of these proofs can be golfed with grw, but that need not be done by this PR.

cf the two preliminary PRs. The changes that are left (almost, because I had to do some more changes after merging master several times) all can't be done with grw (because of defeq abuse or similar).

JovanGerb · 2025-11-21T17:20:31Z

(There's a merge conflict now)

Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>

JovanGerb · 2025-11-22T20:23:39Z

I would prefer it if you did a git merge master to fix the merge conflict, because then I can verify that nothing major has changed in the meantime. If you force push something, for all I know it could be something completely different.

bors r+

YaelDillies · 2025-11-22T20:35:55Z

Sorry but rebasing is useful to me for many other reasons. It's not going away from my workflow. You can use the "Viewed" buttons in the diff view to restrict your attention to the changes that occurred since you last looked at the PR.

mathlib-bors · 2025-11-22T21:25:39Z

Pull request successfully merged into master.

Build succeeded:

…lib4 * 'master' of https://github.com/leanprover-community/mathlib4: (3130 commits) feat(SetTheory/ZFC): add `ZFSet.card` (leanprover-community#29365) feat: grind annotations for `choose_spec` (leanprover-community#31927) chore(scripts): update nolints.json (leanprover-community#31975) feat(Analysis): cos (n * π) = (-1) ^ n (leanprover-community#31971) chore: rename `mul_le_mul_right'` to `mul_le_mul_left` (leanprover-community#30242) chore: update Mathlib dependencies 2025-11-22 (leanprover-community#31955) feat(MeasureTheory): ae-measurability notation wrt non-standard sigma-algebra (leanprover-community#31910) doc: add missing spaces around doc code blocks (leanprover-community#31917) chore: update Mathlib dependencies 2025-11-22 (leanprover-community#31945) chore: shortcut instance for `Nat` to be mul-torsion-free (leanprover-community#31027) doc(Topology/Algebra/Algebra): outdated TODO (leanprover-community#31944) feat(EqHaar): add `addHaar_nnreal_smul` (leanprover-community#31922) chore(Algebra): make invertibleInv an instance (leanprover-community#31916) chore(Algebra): change two statements in CubicDiscriminant (leanprover-community#31912) chore(MeasureTheory): mark `map_dirac` as simp (leanprover-community#31909) feat: `LinearOrder` instance for `Empty` (leanprover-community#31889) chore: deprecate all remaining modules in `Analysis/NormedSpace` (leanprover-community#31913) feat(SimpleGraph): weaker condition for paths in acyclic graphs (leanprover-community#25814) chore: do not set `group` when declaring option (leanprover-community#31888) chore: clean up more unused `Decidable*` instances in types (leanprover-community#31934) ...

YaelDillies mentioned this pull request Oct 5, 2025

[Merged by Bors] - chore: rename mul_le_mul_left/mul_le_mul_right to mul_le_mul_iff_right₀/mul_le_mul_iff_left₀ #28645

Closed

YaelDillies added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Oct 5, 2025

JovanGerb reviewed Oct 5, 2025

View reviewed changes

scripts/nolints_prime_decls.txt Outdated Show resolved Hide resolved

github-actions 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 Oct 12, 2025

YaelDillies force-pushed the mul_le_mul_left branch from 42110be to 44f5d59 Compare October 12, 2025 07:53

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 Oct 12, 2025

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 Oct 13, 2025

YaelDillies force-pushed the mul_le_mul_left branch from 3475345 to 89dea19 Compare October 13, 2025 07:42

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 Oct 13, 2025

YaelDillies mentioned this pull request Oct 13, 2025

[Merged by Bors] - chore: use grw, gcongr more #30508

Closed

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 13, 2025

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 Oct 15, 2025

YaelDillies force-pushed the mul_le_mul_left branch from 77584ea to 668b246 Compare October 17, 2025 14:40

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 Oct 17, 2025

YaelDillies force-pushed the mul_le_mul_left branch from 668b246 to 593d6cc Compare October 17, 2025 14:51

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

github-actions 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 Oct 19, 2025

YaelDillies force-pushed the mul_le_mul_left branch from 762cffd to f720855 Compare October 19, 2025 14:20

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 Oct 19, 2025

YaelDillies force-pushed the mul_le_mul_left branch from f720855 to 45c7eb3 Compare October 19, 2025 14:21

Vierkantor added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 14, 2025

YaelDillies added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 15, 2025

YaelDillies force-pushed the mul_le_mul_left branch 2 times, most recently from 903c787 to 96ab2ad Compare November 18, 2025 09:13

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 18, 2025

Vierkantor approved these changes Nov 20, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Nov 20, 2025

JovanGerb reviewed Nov 20, 2025

View reviewed changes

YaelDillies and others added 8 commits November 21, 2025 18:46

nmul_le_nmul

a9aabff

chore: rename mul_le_mul_right' to mul_le_mul_left

5e2ce38

deprecate

b6412e2

ENNReal.mul_le_mul_left too

977a122

fix

916341f

fix

b19c917

golf

1353331

Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>

typo

0ac1c90

YaelDillies force-pushed the mul_le_mul_left branch from 0b5dfec to 0ac1c90 Compare November 21, 2025 17:46

mathlib-bors bot pushed a commit that referenced this pull request Nov 22, 2025

chore: rename mul_le_mul_right' to mul_le_mul_left (#30242)

b07a584

mathlib-bors bot changed the title ~~chore: rename mul_le_mul_right' to mul_le_mul_left~~ [Merged by Bors] - chore: rename mul_le_mul_right' to mul_le_mul_left Nov 22, 2025

mathlib-bors bot closed this Nov 22, 2025

YaelDillies deleted the mul_le_mul_left branch November 22, 2025 21:39

mathlib-bors bot pushed a commit that referenced this pull request Nov 27, 2025

chore: add deprecations from #30242 (#32172)

bc044be

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary cf85478f35

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

JovanGerb commented Oct 10, 2025

Uh oh!

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

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Oct 13, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Oct 15, 2025

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Nov 20, 2025

Uh oh!

JovanGerb left a comment

Choose a reason for hiding this comment

Uh oh!

JovanGerb Nov 20, 2025

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

JovanGerb Nov 20, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Nov 21, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies commented Nov 21, 2025

Uh oh!

JovanGerb commented Nov 21, 2025

Uh oh!

JovanGerb commented Nov 22, 2025

Uh oh!

YaelDillies commented Nov 22, 2025

Uh oh!

mathlib-bors bot commented Nov 22, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

YaelDillies commented Oct 5, 2025 •

edited

Loading

github-actions bot commented Oct 5, 2025 •

edited

Loading

YaelDillies commented Oct 10, 2025 •

edited

Loading

YaelDillies Nov 21, 2025 •

edited

Loading