chore(ConditionallyCompleteLattice/Indexed): dualize by lua-vr · Pull Request #38938 · leanprover-community/mathlib4

lua-vr · 2026-05-04T19:20:47Z

github-actions · 2026-05-04T19:22:09Z

PR summary e19202a082

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ WithTop.coe_biInf
+ WithTop.coe_biSup
- BddBelow.range_iInf_of_iUnion_range
- IsGLB.ciInf_eq
- IsGLB.ciInf_set_eq
- Set.Ici_ciSup
- WithBot.coe_iInf
- WithBot.coe_iSup
- WithBot.coe_sInf'
- WithBot.coe_sSup'
- WithBot.instInfSet
- WithBot.instSupSet
- WithBot.sSup_empty
- cbiInf_eq_ciInf_subtype
- cbiInf_eq_of_not_forall
- cbiInf_id
- cbiInf_of_not_bddBelow
- ciInf_and
- ciInf_eq_bot_of_bot_mem
- ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
- ciInf_eq_univ_of_not_bddBelow
- ciInf_image
- ciInf_inf_eq
- ciInf_inf_le
- ciInf_le
- ciInf_le_of_le
- ciInf_lt_iff
- ciInf_mono
- ciInf_mono_of_forall_exists
- ciInf_of_not_bddBelow
- ciInf_prod
- ciInf_set_le
- ciInf_subtype
- ciInf_subtype_fun
- ciInf₂_le
- csInf_eq_csInf_of_forall_exists_le
- csInf_eq_of_forall_ge_of_forall_gt_exists_lt
- csInf_eq_univ_of_not_bddBelow
- csInf_image
- csInf_lt_iff
- csInf_lt_of_lt
- csInf_of_not_bddBelow
- csSup_eq_top_of_top_mem
- exists_lt_of_ciInf_lt
- exists_lt_of_csInf_lt
- isGLB_ciInf
- isGLB_ciInf_set
- le_ciInf
- le_ciInf_exists
- le_ciInf_iff
- le_ciInf_set_iff
- map_ciInf
- map_ciInf_set
- map_csInf
- map_csInf'
- u_ciInf
- u_ciInf_set
- u_csInf
- u_csInf'

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.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit e19202a082
Reference commit 72a044471f

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

lua-vr · 2026-05-04T19:23:13Z

 theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
  if_pos <| by simp

+@[to_dual (attr := norm_cast)]


Was there a particular reason for the WithTop ones to not have norm_cast? With this PR, both versions get tagged for norm_cast

Yes, this is probably an oversight. I'm not sure that this is actually a good norm_cast lemma. can you try removing the tag? If something breaks as a result, then we'll know why we need the norm_cast tag.

lua-vr · 2026-05-06T14:33:32Z


 @[deprecated (since := "2026-04-05")] alias ciInf_eq_top_of_top_mem := ciSup_eq_top_of_top_mem

 variable [WellFoundedLT α]


Dual theorems for WellFoundedLT did not get added because the chain of @[to_dual]s to add eventually leads to the WellFounded structure, which does not have a dual. And similarly for ConditionallyCompleteOrderBot

mathlib-merge-conflicts · 2026-05-11T21:53:10Z

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

mathlib-merge-conflicts · 2026-05-15T15:02:38Z

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

mathlib-merge-conflicts · 2026-05-23T17:44:37Z

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

JovanGerb · 2026-05-30T16:35:50Z

Why does this PR depend on the other PR? Can't this be a standalone PR?

mathlib-bors · 2026-05-31T11:30:45Z

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

JovanGerb

Thanks for making this PR! With to_dual PRs, it is best to try to dualize all of the declarations in the files that you are dualizing, because otherwise, we will run into missing to_dual tags in the future. Doing so will make this PR even bigger, so you could maybe split it into a PR doing Basic.lean, and a subsequent one doing Indexed.lean.

JovanGerb · 2026-05-31T14:19:16Z


 open Classical in
+@[to_dual]
 noncomputable instance WithTop.instSupSet [SupSet α] :


Suggested change

noncomputable instance WithTop.instSupSet [SupSet α] :

noncomputable instance [SupSet α] :

Can you put the first part of the file inside a namespace WithTop? Then you can also omit the name of the instance altogether.

That does require dualizing all of the declarations in the section.

JovanGerb · 2026-05-31T14:20:54Z

-    InfSet (WithBot α) :=
-  ⟨(WithTop.instSupSet (α := αᵒᵈ)).sSup⟩
-
 theorem WithTop.sSup_eq [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s)


Is there a reason not to tag this with to_dual?

JovanGerb · 2026-05-31T14:23:23Z

 theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
  if_pos <| by simp

+@[to_dual (attr := norm_cast)]


Yes, this is probably an oversight. I'm not sure that this is actually a good norm_cast lemma. can you try removing the tag? If something breaks as a result, then we'll know why we need the norm_cast tag.

JovanGerb · 2026-05-31T14:31:11Z

  by_cases BddAbove (s ∪ t) <;>
    grind [csSup_union, bddAbove_union, csSup_of_not_bddAbove]

 lemma sSup_iUnion_Iic (f : ι → α) : sSup (⋃ (i : ι), Iic (f i)) = ⨆ i, f i := by


Can you dualize this too?

JovanGerb · 2026-05-31T14:37:00Z

+@[to_dual csInf_eq_of_forall_ge_of_forall_gt_exists_lt /-- Introduction rule to prove that `b` is
+the infimum of `s`: it suffices to check that `b` is smaller than all elements of `s`, and that this
+is not the case of any `w>b`. See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in
+complete lattices. -/]


Suggested change

@[to_dual csInf_eq_of_forall_ge_of_forall_gt_exists_lt /-- Introduction rule to prove that `b` is

the infimum of `s`: it suffices to check that `b` is smaller than all elements of `s`, and that this

is not the case of any `w>b`. See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in

complete lattices. -/]

@[to_dual csInf_eq_of_forall_ge_of_forall_gt_exists_lt

/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`

is smaller than all elements of `s`, and that this is not the case of any `w>b`.

See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/]

I prefer starting the dual comment on a new line if it takes multiple lines, so that it aligns nicely with original comment. This makes it easier to edit both, and to ensure that they actually align. Similarly below

lua-vr · 2026-06-01T07:46:11Z

@JovanGerb Thank you for your comments! This makes sense, I will try to split it for Basic first.

mathlib-merge-conflicts · 2026-06-05T01:26:29Z

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

JovanGerb · 2026-06-21T17:31:35Z

@lua-vr, have you made the new PR already?

lua-vr · 2026-06-21T20:12:04Z

@JovanGerb no, not yet. Feel free to add awaiting-author.

JovanGerb · 2026-07-10T04:09:34Z

I have now created #41558 for using to_dual in Basic

github-actions Bot added the t-order Order theory label May 4, 2026

lua-vr commented May 4, 2026

View reviewed changes

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 4, 2026

lua-vr force-pushed the dualize-indexed branch 3 times, most recently from 4ff10ea to 7590793 Compare May 6, 2026 14:25

lua-vr commented May 6, 2026

View reviewed changes

lua-vr marked this pull request as ready for review May 6, 2026 17:11

lua-vr force-pushed the dualize-indexed branch from d9165c9 to 0aa2584 Compare May 6, 2026 17:19

mathlib-merge-conflicts 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 May 11, 2026

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 May 13, 2026

mathlib-merge-conflicts 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 May 15, 2026

lua-vr force-pushed the dualize-indexed branch from b317858 to 9a752ae Compare May 18, 2026 11:55

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 May 18, 2026

lua-vr force-pushed the dualize-indexed branch from 9a752ae to 5518032 Compare May 18, 2026 14:37

lua-vr mentioned this pull request May 19, 2026

feat(ConditionallyCompleteLattice/Indexed): add binary versions of lemmas #38906

Open

mathlib-merge-conflicts 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 May 23, 2026

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 May 30, 2026

chore: dualize ConditionallyCompleteLattice/Indexed

85654c3

lua-vr force-pushed the dualize-indexed branch 2 times, most recently from c23b520 to b86c675 Compare May 31, 2026 11:26

lua-vr marked this pull request as draft May 31, 2026 11:30

merge upstream

271a91c

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 31, 2026

lua-vr force-pushed the dualize-indexed branch from b86c675 to 271a91c Compare May 31, 2026 11:36

fixes

e19202a

lua-vr marked this pull request as ready for review May 31, 2026 11:52

JovanGerb reviewed May 31, 2026

View reviewed changes

mathlib-merge-conflicts 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 Jun 5, 2026


		@[deprecated (since := "2026-04-05")] alias ciInf_eq_top_of_top_mem := ciSup_eq_top_of_top_mem

		variable [WellFoundedLT α]

	noncomputable instance WithTop.instSupSet [SupSet α] :
	noncomputable instance [SupSet α] :

Uh oh!

Conversation

lua-vr commented May 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary e19202a082

Import changes for modified files

Declarations diff

Uh oh!

lua-vr May 4, 2026 • 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!

JovanGerb May 31, 2026

Choose a reason for hiding this comment

Uh oh!

lua-vr May 6, 2026 • 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!

mathlib-merge-conflicts Bot commented May 11, 2026

Uh oh!

mathlib-merge-conflicts Bot commented May 15, 2026

Uh oh!

mathlib-merge-conflicts Bot commented May 23, 2026

Uh oh!

JovanGerb commented May 30, 2026

Uh oh!

mathlib-bors Bot commented May 31, 2026

Uh oh!

JovanGerb left a comment

Choose a reason for hiding this comment

Uh oh!

JovanGerb May 31, 2026

Choose a reason for hiding this comment

Uh oh!

JovanGerb May 31, 2026

Choose a reason for hiding this comment

Uh oh!

JovanGerb May 31, 2026

Choose a reason for hiding this comment

Uh oh!

JovanGerb May 31, 2026

Choose a reason for hiding this comment

Uh oh!

JovanGerb May 31, 2026

Choose a reason for hiding this comment

Uh oh!

lua-vr commented Jun 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-merge-conflicts Bot commented Jun 5, 2026

Uh oh!

JovanGerb commented Jun 21, 2026

Uh oh!

lua-vr commented Jun 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JovanGerb commented Jul 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

lua-vr commented May 4, 2026 •

edited

Loading

github-actions Bot commented May 4, 2026 •

edited

Loading

lua-vr May 4, 2026 •

edited

Loading

lua-vr May 6, 2026 •

edited

Loading

lua-vr commented Jun 1, 2026 •

edited

Loading

lua-vr commented Jun 21, 2026 •

edited

Loading