[Merged by Bors] - fix(Order): fix simp lemma for with{Top/Bot}{Map/Congr} by wwylele · Pull Request #26787 · leanprover-community/mathlib4

wwylele · 2025-07-05T14:15:28Z

This change includes the following in generated simp lemmas:

-@[simp] theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : 
-  ⇑f.withBotMap = Option.map ⇑f
+@[simp] theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) :
+  ⇑f.withBotMap = WithBot.map ⇑f

@[simp] theorem OrderEmbedding.withTopMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) :
  ⇑f.withTopMap = WithTop.map ⇑f -- unchanged

-@[simp] theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) (a✝ : Option α) : 
-  e.withBotCongr a✝ = Option.map (⇑e) a✝
+@[simp] theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
+  ⇑e.withBotCongr = WithBot.map ⇑e

-@[simp] theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) (a✝ : Option α) : 
-  e.withTopCongr a✝ = Option.map (⇑e) a✝
+@[simp] theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) :
+  ⇑e.withTopCongr = WithTop.map ⇑e

The existing @[simps!] lemma on withTopCongr sends the expression to Equiv.optionCongr, which is hard to work with because it losts WithTop/WithBot tags and Option has fewer lemmas. Add these to preserve WithTop/WithBot tags.

I didn't tag these as @[simp] because it would conflict with existing @[simps!]. But to be honest I don't like the existing simps. Can I remove @[simps! apply] from withTopCongr and promote the new lemma as simp normal form?

The existing @[simps!] lemma on withTopCongr sends expression to Equiv.optionCongr, which is hard to work with because it losts WithTop/WithBot tags and Option has fewer lemmas. Add these to preserve WithTop/WithBot tags.

github-actions · 2025-07-05T14:16:37Z

PR summary 063d2e5dac

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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

Ruben-VandeVelde · 2025-07-05T17:15:00Z

Please do try to replace the existing lemmas, I can't imagine them being used often. Thanks!

wwylele · 2025-07-05T19:09:33Z

After playing around a bit, I decided to instead change the existing withTopCongr_apply lemma (generated from simps) to sending the expression to WithTop.map. A withTopCongr (some ...)) expression will then be further handled by WithTop.map_coe to reach the simplest form.

I don't know about the deprecation policy for this kind of issue. The new good one will take the the name withTopCongr_apply so it isn't compatible with the old one. Is this ok? At least within mathlib this doesn't have much use yet.

Ruben-VandeVelde

Thanks!

maintainer merge

github-actions · 2025-07-07T15:36:14Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

eric-wieser · 2025-07-07T15:39:17Z

Mathlib/Order/Hom/WithTopBot.lean

 def withTopCongr (e : α ≃o β) : WithTop α ≃o WithTop β :=
  { e.toOrderEmbedding.withTopMap with
    toEquiv := e.toEquiv.optionCongr }


I'd argue we should redefine this so that simps does do the right thing; I think in practice that would look like

Suggested change

def withTopCongr (e : α ≃o β) : WithTop α ≃o WithTop β :=

{ e.toOrderEmbedding.withTopMap with

toEquiv := e.toEquiv.optionCongr }

def withTopCongr (e : α ≃o β) : WithTop α ≃o WithTop β where

toFun := WithTop.map e

invFun := WithTop.map e.symm

__ := e.toOrderEmbedding.withTopMap

__ := e.toEquiv.optionCongr

I like it! Just did a quick test that the new simp from this can still correctly simplify e.withTopCongr (WithTop.some ...), so I am using the code as-is

I said it too fast... this leaded to a rabbit hole in OrderEmbedding.withTop/BotCongr's bad def. Currently their generated apply simp don't even have the same signature:

OrderEmbedding.withBotMap_apply simps to Option.map

OrderEmbedding.withTopMap_apply simps to WithTop.map

Guess there is more to fix

wwylele · 2025-07-07T18:56:10Z

I pushed a change to unify the four simp lemmas across OrderEmbedding and OrderIso (see PR description)

Ruben-VandeVelde

Thanks!

maintainer merge

github-actions · 2025-07-10T10:08:40Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

bryangingechen · 2025-07-11T14:05:26Z

Thanks!
bors r+

This change includes the following in generated simp lemmas: ```diff -@[simp] theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : - ⇑f.withBotMap = Option.map ⇑f +@[simp] theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : + ⇑f.withBotMap = WithBot.map ⇑f @[simp] theorem OrderEmbedding.withTopMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : ⇑f.withTopMap = WithTop.map ⇑f -- unchanged -@[simp] theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) (a✝ : Option α) : - e.withBotCongr a✝ = Option.map (⇑e) a✝ +@[simp] theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : + ⇑e.withBotCongr = WithBot.map ⇑e -@[simp] theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) (a✝ : Option α) : - e.withTopCongr a✝ = Option.map (⇑e) a✝ +@[simp] theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : + ⇑e.withTopCongr = WithTop.map ⇑e ```

mathlib-bors · 2025-07-11T15:12:28Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…ommunity#26787) This change includes the following in generated simp lemmas: ```diff -@[simp] theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : - ⇑f.withBotMap = Option.map ⇑f +@[simp] theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : + ⇑f.withBotMap = WithBot.map ⇑f @[simp] theorem OrderEmbedding.withTopMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : ⇑f.withTopMap = WithTop.map ⇑f -- unchanged -@[simp] theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) (a✝ : Option α) : - e.withBotCongr a✝ = Option.map (⇑e) a✝ +@[simp] theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : + ⇑e.withBotCongr = WithBot.map ⇑e -@[simp] theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) (a✝ : Option α) : - e.withTopCongr a✝ = Option.map (⇑e) a✝ +@[simp] theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : + ⇑e.withTopCongr = WithTop.map ⇑e ```

feat(Order): Add apply lemma for withTopCongr/withBotCongr

dc6f796

The existing @[simps!] lemma on withTopCongr sends expression to Equiv.optionCongr, which is hard to work with because it losts WithTop/WithBot tags and Option has fewer lemmas. Add these to preserve WithTop/WithBot tags.

wwylele mentioned this pull request Jul 5, 2025

[Merged by Bors] - feat(RingTheory): decompose archimedean classes of HahnSeries #25970

Closed

7 tasks

github-actions bot added the t-order Order theory label Jul 5, 2025

wwylele added 2 commits July 5, 2025 14:56

remove simps from withTopCongr/withBotCongr

5c42195

Replace with universal apply-lemma

66aa709

Ruben-VandeVelde approved these changes Jul 7, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 7, 2025

eric-wieser reviewed Jul 7, 2025

View reviewed changes

refactor

cabba1f

wwylele changed the title ~~feat(Order): Add apply lemma for withTopCongr/withBotCongr~~ refactor(Order): fix simp lemma for with{Top/Bot}{Map/Congr} Jul 7, 2025

wwylele changed the title ~~refactor(Order): fix simp lemma for with{Top/Bot}{Map/Congr}~~ fix(Order): fix simp lemma for with{Top/Bot}{Map/Congr} Jul 7, 2025

wwylele requested a review from eric-wieser July 7, 2025 21:13

Ruben-VandeVelde approved these changes Jul 10, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jul 11, 2025

mathlib-bors bot changed the title ~~fix(Order): fix simp lemma for with{Top/Bot}{Map/Congr}~~ [Merged by Bors] - fix(Order): fix simp lemma for with{Top/Bot}{Map/Congr} Jul 11, 2025

mathlib-bors bot closed this Jul 11, 2025

wwylele deleted the wwylele-hahn-withtopbot branch September 2, 2025 01:32

-def withTopCongr (e : α ≃o β) : WithTop α ≃o WithTop β :=
-  { e.toOrderEmbedding.withTopMap with
-    toEquiv := e.toEquiv.optionCongr }
+def withTopCongr (e : α ≃o β) : WithTop α ≃o WithTop β where
+  toFun := WithTop.map e
+  invFun := WithTop.map e.symm
+  __ := e.toOrderEmbedding.withTopMap
+  __ := e.toEquiv.optionCongr

Conversation

wwylele commented Jul 5, 2025 • edited by Ruben-VandeVelde Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 063d2e5dac

Import changes for modified files

Declarations diff

Uh oh!

Ruben-VandeVelde commented Jul 5, 2025

Uh oh!

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

Uh oh!

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jul 7, 2025

Uh oh!

eric-wieser Jul 7, 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!

wwylele Jul 7, 2025

Choose a reason for hiding this comment

Uh oh!

wwylele Jul 7, 2025

Choose a reason for hiding this comment

Uh oh!

wwylele commented Jul 7, 2025

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jul 10, 2025

Uh oh!

bryangingechen commented Jul 11, 2025

Uh oh!

mathlib-bors bot commented Jul 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

wwylele commented Jul 5, 2025 •

edited by Ruben-VandeVelde

Loading

github-actions bot commented Jul 5, 2025 •

edited

Loading

wwylele commented Jul 5, 2025 •

edited

Loading

eric-wieser Jul 7, 2025 •

edited

Loading