[Merged by Bors] - chore(Data/Finset/Lattice/Fold): use `to_dual` by gasparattila · Pull Request #37047 · leanprover-community/mathlib4

gasparattila · 2026-03-23T17:11:15Z

This PR uses the @[to_dual] attribute to generate dual lemmas about Finset.sup. The lemmas about sdiff and himp are skipped, as HeytingAlgebra is not yet tagged with @[to_dual].

To improve the consistency between dual lemmas, several changes are made:

tag inf_insert with @[grind =]
rename le_inf_const_le to le_inf_const
tag inf_union with @[grind _=_]
tag inf_mono_fun with @[grind ←]
tag inf_mono with @[grind ←]
tag inf_attach with @[simp]
add le_inf_of_directed_le
add inf_eq_top_of_isEmpty
add inf_mem_of_nonempty
add inf'_mono_fun
rename comp_sup_eq_sup_comp_of_nonempty to apply_sup_eq_sup_comp_of_nonempty and add apply_inf_eq_inf_comp_of_nonempty

github-actions · 2026-03-23T17:12:24Z

PR summary ff84feb246

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ apply_sup_eq_sup_comp_of_nonempty
- Nonempty.inf_eq_bot_iff
- _root_.List.foldr_inf_eq_inf_toFinset
- _root_.map_finset_inf
- _root_.map_finset_inf'
- codisjoint_inf_left
- codisjoint_inf_right
- coe_inf'
- coe_inf_of_nonempty
- comp_inf'_eq_inf'_comp
- comp_inf_eq_inf_comp
- comp_inf_eq_inf_comp_of_is_total
- compl_inf
- exists_inf_eq_iInf
- exists_inf_le
- exists_mem_eq_inf
- exists_mem_eq_inf'
- inf
- inf'
- inf'_apply
- inf'_comm
- inf'_comp_eq_image
- inf'_comp_eq_map
- inf'_congr
- inf'_cons
- inf'_const
- inf'_eq_inf
- inf'_eq_of_forall
- inf'_image
- inf'_induction
- inf'_insert
- inf'_le
- inf'_le_iff
- inf'_le_of_le
- inf'_lt_iff
- inf'_map
- inf'_mem
- inf'_mono
- inf'_singleton
- inf'_sup_distrib_left
- inf'_sup_distrib_right
- inf'_union
- inf_apply
- inf_attach
- inf_coe
- inf_comm
- inf_congr
- inf_cons
- inf_const
- inf_def
- inf_disjSum
- inf_dite_neg_le
- inf_dite_pos_le
- inf_empty
- inf_eq_bot_iff
- inf_eq_iInf
- inf_eq_sInf_image
- inf_eq_top_iff
- inf_erase_top
- inf_id_eq_sInf
- inf_image
- inf_induction
- inf_inf
- inf_insert
- inf_ite
- inf_le
- inf_le_iff
- inf_le_of_le
- inf_lt_iff
- inf_map
- inf_mem
- inf_mono
- inf_mono_fun
- inf_of_mem
- inf_singleton
- inf_sup_distrib_left
- inf_sup_distrib_right
- inf_top
- inf_union
- isGLB_inf
- isGLB_inf'
- isGLB_inf_id
- le_inf'_iff
- le_inf_iff
- lt_inf'_iff
- lt_inf_iff
- ofDual_inf
- ofDual_inf'
- toDual_inf
- toDual_inf'

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

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

JovanGerb

Could you clarify in the PR description which changes were made because they were already there on the dual side? Currently it looks like you added some tags for orthogonal reasons.

mathlib-merge-conflicts · 2026-03-27T20:49:40Z

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

This PR uses the `@[to_dual]` attribute to generate dual lemmas about `Finset.sup`. The lemmas about `sdiff` and `himp` are skipped, as `HeytingAlgebra` is not yet tagged with `@[to_dual]`. Other changes: - tag `inf_insert` with `@[grind =]` - rename `le_inf_const_le` to `le_inf_const` - tag `inf_union` with `@[grind _=_]` - tag `inf_mono_fun` with `@[grind ←]` - tag `inf_mono` with `@[grind ←]` - tag `inf_attach` with `@[simp]` - add `le_inf_of_directed_le` - add `inf_eq_top_of_isEmpty` - add `inf_mem_of_nonempty` - rename `comp_sup_eq_sup_comp_of_is_total` to `comp_sup_eq_sup_comp_of_linearOrder` (and similarly for the `inf` version) - add `inf'_mono_fun` - add `comp_inf_eq_inf_comp_of_nonempty`

gasparattila · 2026-04-08T10:07:57Z

-awaiting-author

JovanGerb · 2026-04-08T13:36:38Z

+-- TODO: `@[to_dual]` should translate the docstring generated by `alias`
 protected alias ⟨_, sup_le⟩ := Finset.sup_le_iff

+@[to_dual existing sup_le]
+protected alias ⟨_, le_inf⟩ := Finset.le_inf_iff


By the way, I've opened leanprover-community/batteries#1763 to start supporting this feature.

bryangingechen

Thanks!
bors r+

This PR uses the `@[to_dual]` attribute to generate dual lemmas about `Finset.sup`. The lemmas about `sdiff` and `himp` are skipped, as `HeytingAlgebra` is not yet tagged with `@[to_dual]`. To improve the consistency between dual lemmas, several changes are made: - tag `inf_insert` with `@[grind =]` - rename `le_inf_const_le` to `le_inf_const` - tag `inf_union` with `@[grind _=_]` - tag `inf_mono_fun` with `@[grind ←]` - tag `inf_mono` with `@[grind ←]` - tag `inf_attach` with `@[simp]` - add `le_inf_of_directed_le` - add `inf_eq_top_of_isEmpty` - add `inf_mem_of_nonempty` - add `inf'_mono_fun` - rename `comp_sup_eq_sup_comp_of_nonempty` to `apply_sup_eq_sup_comp_of_nonempty` and add `apply_inf_eq_inf_comp_of_nonempty`

mathlib-bors · 2026-04-08T19:55:10Z

Pull request successfully merged into master.

Build succeeded:

…37047) This PR uses the `@[to_dual]` attribute to generate dual lemmas about `Finset.sup`. The lemmas about `sdiff` and `himp` are skipped, as `HeytingAlgebra` is not yet tagged with `@[to_dual]`. To improve the consistency between dual lemmas, several changes are made: - tag `inf_insert` with `@[grind =]` - rename `le_inf_const_le` to `le_inf_const` - tag `inf_union` with `@[grind _=_]` - tag `inf_mono_fun` with `@[grind ←]` - tag `inf_mono` with `@[grind ←]` - tag `inf_attach` with `@[simp]` - add `le_inf_of_directed_le` - add `inf_eq_top_of_isEmpty` - add `inf_mem_of_nonempty` - add `inf'_mono_fun` - rename `comp_sup_eq_sup_comp_of_nonempty` to `apply_sup_eq_sup_comp_of_nonempty` and add `apply_inf_eq_inf_comp_of_nonempty`

github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Mar 23, 2026

gasparattila mentioned this pull request Mar 23, 2026

[Merged by Bors] - chore(Data/Set/Finite/Lattice): use to_dual #37051

Closed

1 task

gasparattila force-pushed the to_dual-Finset.sup branch from 0e9b416 to f3364b8 Compare March 23, 2026 18:15

gasparattila mentioned this pull request Mar 23, 2026

[Merged by Bors] - chore(Data/Finset/Lattice/Prod): use to_dual #37052

Closed

1 task

JovanGerb reviewed Mar 25, 2026

View reviewed changes

gasparattila force-pushed the to_dual-Finset.sup branch from f3364b8 to 908db92 Compare March 25, 2026 21:48

gasparattila mentioned this pull request Mar 25, 2026

chore(Data/Finset/Lattice/Fold): rename comp_sup_* to apply_sup_* #37185

Open

1 task

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 Mar 27, 2026

gasparattila force-pushed the to_dual-Finset.sup branch from cb0c8a4 to e79a7ea Compare March 27, 2026 21:34

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 Mar 27, 2026

mathlib-triage bot assigned joneugster Mar 29, 2026

bryangingechen added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 7, 2026

gasparattila added 5 commits April 8, 2026 12:04

update

fc0b24d

Add TODO for alias

e3a0581

rename

ad30cff

Remove rename

4264770

gasparattila force-pushed the to_dual-Finset.sup branch from 7777655 to 4264770 Compare April 8, 2026 10:04

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 8, 2026

JovanGerb reviewed Apr 8, 2026

View reviewed changes

bryangingechen approved these changes Apr 8, 2026

View reviewed changes

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Apr 8, 2026

mathlib-bors bot changed the title ~~chore(Data/Finset/Lattice/Fold): use to_dual~~ [Merged by Bors] - chore(Data/Finset/Lattice/Fold): use to_dual Apr 8, 2026

mathlib-bors bot closed this Apr 8, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(Data/Finset/Lattice/Fold): use `to_dual`#37047

[Merged by Bors] - chore(Data/Finset/Lattice/Fold): use `to_dual`#37047
gasparattila wants to merge 5 commits intoleanprover-community:masterfrom
gasparattila:to_dual-Finset.sup

gasparattila commented Mar 23, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Mar 23, 2026 •

edited

Loading

Declarations diff

Uh oh!

JovanGerb left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Mar 27, 2026

Uh oh!

gasparattila commented Apr 8, 2026

Uh oh!

JovanGerb Apr 8, 2026

Uh oh!

bryangingechen left a comment

Uh oh!

mathlib-bors bot commented Apr 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

gasparattila commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ff84feb246

Import changes for modified files

Declarations diff

Uh oh!

JovanGerb left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Mar 27, 2026

Uh oh!

gasparattila commented Apr 8, 2026

Uh oh!

JovanGerb Apr 8, 2026

Choose a reason for hiding this comment

Uh oh!

bryangingechen left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Apr 8, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

gasparattila commented Mar 23, 2026 •

edited

Loading

github-actions bot commented Mar 23, 2026 •

edited

Loading