[Merged by Bors] - chore(Tactic/GCongr): move `@[gcongr]` tags around by urkud · Pull Request #9393 · leanprover-community/mathlib4

urkud · 2024-01-01T17:45:42Z

Add import Mathlib.Tactic.GCongr.Core
to Algebra/Order/Ring/Lemmas.
Move most @[gcongr] tags next to the lemmas.

Is there a better home for setting up positivity
as a gcongr discharger?
What should we do with Nat division lemmas?

* Add `import Mathlib.Tactic.GCongr.Core` to `Algebra/Order/Ring/Lemmas`. * Move most `@[gcongr]` tags next to the lemmas.

This was noticed in the discussion around #9393.

Mathlib/Algebra/Order/Field/Basic.lean

Mathlib/Tactic/GCongr.lean

Parcly-Taxel

Is there a better home for setting up positivity as a gcongr discharger?

I think the current setup is fine enough.

urkud · 2024-01-08T00:58:36Z

Is there a better home for setting up positivity as a gcongr discharger?

I think the current setup is fine enough.

It's a footgun: gcongr kind of works without importing Mathlib.Tactic.GCongr but doesn't use positivity. To reduce damage, we can import this file very early as soon as both Positivity.Core and GCongr.Core are imported. OTOH, we already have a similar footgun with Positivity.Core vs Positivity, so maybe the right way to solve the issue is to add documentation to gcongr and positivity ("if the tactic fails, first make sure that your file imports ...").

Parcly-Taxel · 2024-01-08T01:05:07Z

so maybe the right way to solve the issue is to add documentation to gcongr and positivity ("if the tactic fails, first make sure that your file imports ...").

Just solve the issue as you see fit, then.

hrmacbeth · 2024-01-31T05:04:02Z

LGTM, modulo: did this get resolved?

I'm good with importing positivity as early as possible. Should I ask on Zulip for other opinions?

YaelDillies · 2024-02-02T09:13:01Z

Yes, negatively. positivity can't be imported earlier than Field because of the norm_num support at the core of the tactic. So #10140 only moves the extensions that depend on Field anyway. Further, Tactic.Positivity.Basic imports extra cast material that is unimportable in most of the algebraic order hierarchy, so we must restrict to importing only Tactic.Positivity.Core there.

Parcly-Taxel · 2024-02-06T01:11:06Z

#10140 has been merged. You can adapt this PR to it.

urkud · 2024-02-06T23:00:18Z

Merged master, fixed compile.

Mathlib/Algebra/Order/Field/Basic.lean

YaelDillies · 2024-02-07T09:36:13Z

Mathlib/Algebra/Order/Field/Power.lean

  (zpow_strictMono hx).lt_iff_lt
 #align zpow_lt_iff_lt zpow_lt_iff_lt

+@[gcongr] alias ⟨_, zpow_lt_of_lt⟩ := zpow_lt_iff_lt


Suggested change

@[gcongr] alias ⟨_, zpow_lt_of_lt⟩ := zpow_lt_iff_lt

@[gcongr] alias ⟨_, GCongr.zpow_lt_of_lt⟩ := zpow_lt_iff_lt

It doesn't make sense to me to put this in the GCongr namespace for two reasons:

We don't have much else there, especially not many lemmas.

These declarations existed already and were not in that namespace, so we would have to add an alias and a deprecation, but that seems silly.

I like the idea of moving auxiliary lemmas that exist only because gcongr can't handle Monotone/StrictMono/Iff lemmas to the GCongr namespace.

Mathlib/Data/Nat/Cast/Order.lean

Mathlib/Algebra/Order/Field/Power.lean

Mathlib/Data/Nat/Cast/Order.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

YaelDillies

maintainer merge

github-actions · 2024-02-11T08:14:21Z

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

Vierkantor

LGTM, thanks!

bors r+

* Add `import Mathlib.Tactic.GCongr.Core` to `Algebra/Order/Ring/Lemmas`. * Move most `@[gcongr]` tags next to the lemmas. See [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.2FTactic.2FGCongr) Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

mathlib-bors · 2024-02-12T10:30:14Z

Pull request successfully merged into master.

Build succeeded:

* Add `import Mathlib.Tactic.GCongr.Core` to `Algebra/Order/Ring/Lemmas`. * Move most `@[gcongr]` tags next to the lemmas. See [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.2FTactic.2FGCongr) Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

chore(Tactic/GCongr): move @[gcongr] tags around

13f6269

* Add `import Mathlib.Tactic.GCongr.Core` to `Algebra/Order/Ring/Lemmas`. * Move most `@[gcongr]` tags next to the lemmas.

urkud added awaiting-review t-meta Tactics, attributes or user commands RFC Request for comment t-algebra Algebra (groups, rings, fields, etc) labels Jan 1, 2024

urkud requested a review from hrmacbeth January 1, 2024 17:47

Parcly-Taxel added a commit that referenced this pull request Jan 2, 2024

gcongr currently fails here, but #9393 should fix it

8a2670d

This was referenced Jan 2, 2024

[Merged by Bors] - feat: counting elements in an interval with given residue #9348

Closed

[Merged by Bors] - feat: deprecate div_le_div_of_le_of_nonneg #9399

Closed

mathlib-bors bot pushed a commit that referenced this pull request Jan 4, 2024

feat: deprecate div_le_div_of_le_of_nonneg (#9399)

b6aa685

This was noticed in the discussion around #9393.

Parcly-Taxel reviewed Jan 5, 2024

View reviewed changes

Mathlib/Algebra/Order/Field/Basic.lean Outdated Show resolved Hide resolved

Parcly-Taxel reviewed Jan 5, 2024

View reviewed changes

Mathlib/Tactic/GCongr.lean Outdated Show resolved Hide resolved

Update Mathlib/Algebra/Order/Field/Basic.lean

ad4c957

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 6, 2024

urkud added 3 commits January 7, 2024 11:15

Merge branch 'master' into YK-move-gcongr

e6d7f07

Move the remaining attributes

e715939

Reduce imports

ab49870

urkud added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. RFC Request for comment labels Jan 7, 2024

urkud requested a review from Parcly-Taxel January 7, 2024 22:10

Update GCongr.lean

61dc589

Parcly-Taxel approved these changes Jan 8, 2024

View reviewed changes

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 9, 2024

Merge branch 'master' into YK-move-gcongr

9ef3d31

ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jan 9, 2024

urkud added 6 commits February 5, 2024 20:51

Merge branch 'master' into YK-move-gcongr

cc0b7fd

Partially fix

c0529a3

Fix

f2e8db5

Fix archive

378f575

Fix a test

b43b75b

Update noshake

bd221d5

YaelDillies reviewed Feb 7, 2024

View reviewed changes

j-loreaux mentioned this pull request Feb 9, 2024

[Merged by Bors] - chore: add fun_prop attribute to various continuity lemmas #10369

Closed

urkud added 2 commits February 10, 2024 08:27

Merge branch 'master' into YK-move-gcongr

78bbe9d

Move aux lemmas to the GCongr namespace

7c364f5

YaelDillies reviewed Feb 10, 2024

View reviewed changes

Mathlib/Algebra/Order/Field/Power.lean Outdated Show resolved Hide resolved

YaelDillies reviewed Feb 10, 2024

View reviewed changes

Mathlib/Data/Nat/Cast/Order.lean Outdated Show resolved Hide resolved

urkud and others added 2 commits February 10, 2024 15:55

Update Mathlib/Algebra/Order/Field/Power.lean

252dde4

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Fix comment

551f68e

YaelDillies approved these changes Feb 11, 2024

View reviewed changes

Vierkantor approved these changes Feb 12, 2024

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Feb 12, 2024

mathlib-bors bot changed the title ~~chore(Tactic/GCongr): move @[gcongr] tags around~~ [Merged by Bors] - chore(Tactic/GCongr): move @[gcongr] tags around Feb 12, 2024

mathlib-bors bot closed this Feb 12, 2024

mathlib-bors bot deleted the YK-move-gcongr branch February 12, 2024 10:30

ericrbg mentioned this pull request Feb 22, 2024

[Merged by Bors] - feat(Finset): add gcongr attributes #9520

Closed

	@[gcongr] alias ⟨_, zpow_lt_of_lt⟩ := zpow_lt_iff_lt
	@[gcongr] alias ⟨_, GCongr.zpow_lt_of_lt⟩ := zpow_lt_iff_lt

Conversation

urkud commented Jan 1, 2024 • edited by Parcly-Taxel Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Parcly-Taxel left a comment

Choose a reason for hiding this comment

Uh oh!

urkud commented Jan 8, 2024

Uh oh!

Parcly-Taxel commented Jan 8, 2024

Uh oh!

hrmacbeth commented Jan 31, 2024

Uh oh!

YaelDillies commented Feb 2, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Parcly-Taxel commented Feb 6, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

urkud commented Feb 6, 2024

Uh oh!

Uh oh!

YaelDillies Feb 7, 2024

Choose a reason for hiding this comment

Uh oh!

j-loreaux Feb 7, 2024

Choose a reason for hiding this comment

Uh oh!

urkud Feb 10, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Feb 11, 2024

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Feb 12, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

urkud commented Jan 1, 2024 •

edited by Parcly-Taxel

Loading

YaelDillies commented Feb 2, 2024 •

edited

Loading

Parcly-Taxel commented Feb 6, 2024 •

edited

Loading