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

YaelDillies · 2025-10-13T15:21:03Z

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.

Annoyingly, grw is basically unusable with strict inequalities (it often leaves an unprovable goal since it doesn't know about lt_of_le_of_lt nor lt_of_lt_of_le, but only lt_trans). This means that I must fall back to gcongr; exact strict_ineq many times where I would instead have liked to do grw [strict_ineq].

github-actions · 2025-10-13T15:22:16Z

PR summary 2528a23415

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ GCongr.ofNat_le_ofNat
+ card_nonuniformWitnesses_le
+ repr_le_repr
+ repr_lt_repr
+ ruzsaSzemerediNumberNat_le_ruzsaSzemerediNumberNat

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

grunweg

Thank you for doing this huge change! I reviewed the first 101 files so far (will continue later, also when you have fixed the build more). I like most of these changes, think we should benchmark this just in case, and have a few comments when I'm not as sure or need to be convinced this is good.

Mathlib/Algebra/MonoidAlgebra/Degree.lean

Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

Mathlib/Algebra/Order/Interval/Set/Monoid.lean

Mathlib/Algebra/Polynomial/BigOperators.lean

Mathlib/Algebra/Polynomial/Degree/Definitions.lean

Mathlib/Analysis/Convex/Gauge.lean

Mathlib/Analysis/Normed/Order/UpperLower.lean

mathlib4-merge-conflict-bot · 2025-10-15T17:43:59Z

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

grunweg

Reviewed the rest (except for 5 files); I'll do one last pass when you have fixed the build and my comments so far. Thanks a lot for doing this!

Mathlib/Combinatorics/SetFamily/KruskalKatona.lean

Mathlib/Data/Nat/Count.lean

Mathlib/Data/NNReal/Defs.lean

Mathlib/Data/Nat/Dist.lean

Mathlib/Data/Nat/Factorization/Basic.lean

Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Mathlib/Probability/Kernel/Disintegration/Basic.lean

Mathlib/RingTheory/PowerSeries/Order.lean

grunweg · 2025-10-16T16:48:39Z

Assuming CI is happy, I have no further review comments than the ones above. Let's benchmark this and then merge soon!

YaelDillies · 2025-10-16T17:02:56Z

I believe I have replied to all your comments, or rather exhibited a section of answers from the equivalence class of comments. Let's bench too:

!bench

grunweg · 2025-10-16T22:44:30Z

!bench

grunweg · 2025-10-16T22:44:45Z

IIRC, the bot only picks up comments which contain this exact string, and nothing else.

grunweg · 2025-10-16T22:46:53Z

@JovanGerb Do you mind briefly checking the new gcongr lemmas introduced in this PR? I'm pretty sure they're fine, but don't know if there's anything that could go wrong. Thank you!

leanprover-bot · 2025-10-16T23:21:20Z

Here are the benchmark results for commit dd3f9dd.
There were no significant changes against commit 6b1d0f0.

github-actions · 2025-10-16T23:21:56Z

File	Instructions	%
`build`	-572.449⬝10⁹	(-0.35%)
`lint`	-144.94⬝10⁹	(-2.18%)
`Mathlib.Data.Nat.Dist`	+3.888⬝10⁹	(+52.99%)
`Mathlib.Algebra.MvPolynomial.Degrees`	+2.442⬝10⁹	(+8.23%)

4 files, Instructions +1.0⬝10⁹

File	Instructions	%
`Mathlib.Probability.Kernel.Disintegration.Basic`	+1.967⬝10⁹	(+14.56%)
`Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper`	+1.805⬝10⁹	(+2.42%)
`Mathlib.NumberTheory.AbelSummation`	+1.306⬝10⁹	(+3.36%)
`Mathlib.Analysis.Normed.Operator.NNNorm`	+1.53⬝10⁹	(+3.74%)

File	Instructions	%
`Mathlib.Tactic.Common`	-1.59⬝10⁹	(-21.34%)
`Mathlib.MeasureTheory.Function.SimpleFuncDenseLp`	-2.216⬝10⁹	(-2.05%)
CI run Lakeprof report

JovanGerb

Thanks for making this PR. Most gcongr tags look good, I only suggest a change for the opow one.

Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean

JovanGerb · 2025-10-16T23:23:37Z

Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

  | n + 1 => by rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries]

+@[gcongr]
 theorem sqrtTwoAddSeries_monotone_left {x y : ℝ} (h : x ≤ y) :


The lemma name should say mono instead of monotone, but I guess that's not for this PR.

Let's make that a follow-up PR!

Feel free to open a PR, Jovan :)

Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean

Mathlib/Data/Int/Basic.lean

Mathlib/Data/Nat/Count.lean

JovanGerb · 2025-10-16T23:37:05Z

Mathlib/SetTheory/Ordinal/Exponential.lean

 alias isLimit_opow_left := isSuccLimit_opow_left

+@[gcongr]
 theorem opow_le_opow_right {a b c : Ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) : a ^ b ≤ a ^ c := by


I suggest tagging opow_le_opow instead of the right version, as it is more general.

As Heather explained, gcongr needs both (use case being monotonicity of multiplication). I'll tag opow_le_opow too

I claim that if you tag opow_le_opow, then you can safely drop the tag from the right version

If Heather explained otherwise, then that explanation is now out of date.

Sorry, I wasn't aware you had made the change to gcongr. That would have been good to mention the first time around!

grunweg · 2025-10-17T09:17:38Z

Thanks for the quick review, Jovan! With the benchmark results being in, I'm happy this PR with all "somewhat controversial parts removed". If you

remove the instance removal
remove the \forall changes from this PR,

I'll merge the rest directly. Optionally, waiting on a zulip consensus on the style guide thread is another option.

YaelDillies · 2025-10-17T12:16:17Z

See #30632

grunweg · 2025-10-17T12:39:05Z

Thank you for the prompt response and agreeing to split this PR. This subset of changes looks uncontroversial, so I'm happy to merge it directly (once CI has finished).

grunweg · 2025-10-17T12:51:46Z

bors merge

JovanGerb · 2025-10-17T13:11:37Z

opow_le_opow_right is still unnecessarily tagged with @[gcongr]

grunweg · 2025-10-17T13:17:43Z

Sorry for that. Would you like to make a follow-up PR; if it builds, I'll happily merge it!

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.

mathlib-bors · 2025-10-17T14:09:08Z

Build failed (retrying...):

Post-Build Step

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.

mathlib-bors · 2025-10-17T15:39:53Z

Pull request successfully merged into master.

Build succeeded:

This tag was accidentally added in #30508, but it is redundant

YaelDillies mentioned this pull request Oct 13, 2025

chore: rename mul_le_mul_right' to mul_le_mul_left #30242

Open

2 tasks

YaelDillies added the awaiting-CI label Oct 13, 2025

YaelDillies requested a review from JovanGerb October 13, 2025 15:22

YaelDillies force-pushed the more_grw_gcongr branch 5 times, most recently from 5890999 to cd8c2c8 Compare October 14, 2025 09:01

YaelDillies mentioned this pull request Oct 14, 2025

[Merged by Bors] - chore(*): use gcongr/grw #30561

Closed

grunweg self-assigned this Oct 15, 2025

grunweg reviewed Oct 15, 2025

View reviewed changes

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 more_grw_gcongr branch from cd8c2c8 to 1d846f4 Compare October 16, 2025 08:11

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

grunweg reviewed Oct 16, 2025

View reviewed changes

YaelDillies force-pushed the more_grw_gcongr branch from f05f9a7 to fbd43e4 Compare October 16, 2025 15:25

github-actions bot removed the awaiting-CI label Oct 16, 2025

JovanGerb approved these changes Oct 16, 2025

View reviewed changes

chore: use grw, gcongr more

e56245d

YaelDillies force-pushed the more_grw_gcongr branch from 69c81af to e56245d Compare October 17, 2025 12:13

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Oct 17, 2025

mathlib-bors bot changed the title ~~chore: use grw, gcongr more~~ [Merged by Bors] - chore: use grw, gcongr more Oct 17, 2025

mathlib-bors bot closed this Oct 17, 2025

YaelDillies deleted the more_grw_gcongr branch October 17, 2025 15:41

JovanGerb mentioned this pull request Oct 18, 2025

[Merged by Bors] - chore: remove @[gcongr] from opow_le_opow_right #30651

Closed

mathlib-bors bot pushed a commit that referenced this pull request Oct 18, 2025

chore: remove @[gcongr] from opow_le_opow_right (#30651)

a93525e

This tag was accidentally added in #30508, but it is redundant

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

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

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 2528a23415

Import changes for modified files

Declarations diff

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

grunweg commented Oct 16, 2025

Uh oh!

YaelDillies commented Oct 16, 2025

Uh oh!

grunweg commented Oct 16, 2025

Uh oh!

grunweg commented Oct 16, 2025

Uh oh!

grunweg commented Oct 16, 2025

Uh oh!

leanprover-bot commented Oct 16, 2025

Uh oh!

github-actions bot commented Oct 16, 2025

Uh oh!

JovanGerb left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Uh oh!

YaelDillies commented Oct 17, 2025

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

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

YaelDillies commented Oct 13, 2025 •

edited

Loading

github-actions bot commented Oct 13, 2025 •

edited

Loading

grunweg commented Oct 17, 2025 •

edited

Loading