feat(Order/CompleteLattice): more lemmas about membership under lattice operations by artie2000 · Pull Request #44253 · leanprover-community/mathlib4

artie2000 · 2026-09-27T18:08:35Z

Add generic lemmas relating membership to lattice operations assuming IsMemLE

depends on: feat(Order/Lattice): generic lemmas about membership under lattice operations #44353
depends on: chore(Order): move Order/CompleteLattice/SetLike.lean to more descriptive location #44355

github-actions · 2026-09-27T18:10:21Z

PR summary c0384d7847

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.CompleteLattice.SetLike	694	279	-415 (-59.80%)

Import changes for all files

Files	Import difference
`Mathlib.Order.CompleteSublattice`	-693
`Mathlib.Order.CompleteLattice.SetLike` `Mathlib.SetTheory.Descriptive.Tree`	-415
`Mathlib.Order.Lattice.SetLike` (new file)	278
`Mathlib.Order.CompleteSublattice.Basic`	693
`Mathlib.Order.CompleteSublattice.SetLike` (new file)	694

Declarations diff (regex)

+ IsMemLE
+ IsMemLE.exists_of_lt
+ IsMemLE.le_iff
+ IsMemLE.lt_iff_le_and_exists
+ IsMemLE.not_le_iff_exists
+ exists_mem_notMem_of_lt
+ instance (α : Type*) : IsMemLE (Set α) α
+ instance [Membership B A] : letI := LE.ofMembership A; IsMemLE A B
+ lt_iff_le_and_exists_mem_notMem
+ mem_of_le_of_mem
+ mem_of_mem_bot
+ mem_of_mem_inf_left
+ mem_of_mem_inf_right
+ mem_sSup_of_exists
+ mem_sSup_of_mem
+ mem_sup_left
+ mem_sup_of_mem_or_mem
+ mem_sup_right
+ mem_top_of_mem
+ not_le_iff_exists_mem_notMem
- exists_of_lt
- instance (α : Type*) : IsConcreteLE (Set α) α
- instance [Membership B A] : letI := LE.ofMembership A; IsConcreteLE A B
- lt_iff_le_and_exists
- not_le_iff_exists
--++ mem_subtype

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.

Declarations diff (Lean -- stale, waiting for the new build)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit cf35d38).

+8 new declarations
−0 removed declarations

+SetLike.mem_and_mem_of_mem_inf
+SetLike.mem_bot_of_mem
+SetLike.mem_of_mem_inf_left
+SetLike.mem_of_mem_inf_right
+SetLike.mem_sup
+SetLike.mem_sup_left
+SetLike.mem_sup_right
+SetLike.mem_top_of_mem

No changes to strong technical debt.
No changes to weak technical debt.

Current commit c0384d7847
Reference commit 3c58f3bd8f

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

note: file Mathlib/Order/CompleteSublattice.lean` was renamed to `Mathlib/Order/CompleteSublattice/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

github-actions · 2026-09-27T18:10:31Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

JovanGerb · 2026-09-28T11:47:19Z

+lemma mem_of_mem_inf_right {x : B} (h : x ∈ p ⊓ q) : x ∈ q :=
+  mem_of_le_of_mem inf_le_right h
+
+lemma mem_and_mem_of_mem_inf {x : B} (h : x ∈ p ⊓ q) : x ∈ p ∧ x ∈ q :=


Are you sure we need this lemma? It seems a bit redundant.

it's there to be annotated with membership (#42342) in a future PR
I can remove for now?

Even then I would think this lemma is redundant. How would you tag it that can't be done with the two lemmas above?

well, I'd tag it instead of tagging the two lemmas above
to limit the amount of branching that grind needs to do

I don't understand how that affects branching. And grind tags come in many forms - which one were you considering adding?

yeah you're right I'll remove
grind in this case we'd want to fire forward

mathlib-dependent-issues · 2026-09-28T11:50:30Z

This PR/issue depends on:

feat(Order/Lattice): generic lemmas about membership under lattice operations #44353
chore(Order): move Order/CompleteLattice/SetLike.lean to more descriptive location #44355
By Dependent Issues (🤖). Happy coding!

JovanGerb · 2026-09-28T19:21:46Z

+theorem mem_of_mem_inf_right {x : B} (h : x ∈ p ⊓ q) : x ∈ q :=
+  mem_of_le_of_mem inf_le_right h
+
+theorem mem_and_mem_of_mem_inf {x : B} (h : x ∈ p ⊓ q) : x ∈ p ∧ x ∈ q :=


It would make more sense to me if this was an iff lemma, because then you would be able to rewrite with it.

Then, after we get #42316, we could tag mem_inf with @[simp], and remove the @[simp] tag from Set.mem_inter, Finset.mem_inter and ZFSet.mem_inter.

it's not an iff in this generality
iff needs IsMemInf from #43726

and yes indeed once that's added we can remove the more specific lemmas - see Zulip thread https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Abstracting.20the.20substructure.20lattice.20construction/with/627416450 for the idea

Removed theorem mem_and_mem_of_mem_inf from SemilatticeInf.

artie2000 · 2026-09-30T12:13:06Z

this PR needs file reorganisation after #43253
for now look at the new PR #44353

mathlib-merge-conflicts · 2026-10-09T13:00:43Z

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

mathlib-merge-conflicts · 2026-10-24T17:45:57Z

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

initial commit

cf35d38

github-actions Bot added the t-data Data (lists, quotients, numbers, etc) label Sep 27, 2026

artie2000 added the WIP Work in progress label Sep 27, 2026

update, add dependency

c1fcb66

artie2000 changed the title ~~WIP SetLike Lattice lemmas~~ feat(Data/SetLike): generic lemmas about membership under lattice operations Sep 28, 2026

JovanGerb reviewed Sep 28, 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 Sep 28, 2026

move

ed2cdf3

artie2000 mentioned this pull request Sep 28, 2026

feat(Data/SetLike): lattice membership typeclasses for Min and Max #43726

Draft

1 task

Merge branch 'master' into setlike_lattice_lemmas

1fee881

artie2000 removed the WIP Work in progress label Sep 28, 2026

JovanGerb reviewed Sep 28, 2026

View reviewed changes

artie2000 and others added 3 commits September 28, 2026 23:24

remove redundant lemma

e6a5688

Removed theorem mem_and_mem_of_mem_inf from SemilatticeInf.

Merge branch 'master' into setlike_lattice_lemmas

71b39d3

move content

d580073

artie2000 changed the title ~~feat(Data/SetLike): generic lemmas about membership under lattice operations~~ feat(Order/CompleteLattice): generic lemmas about membership under lattice operations Sep 30, 2026

reorganise files

04974d0

github-actions Bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Sep 30, 2026

fix imports

7aadeeb

artie2000 changed the title ~~feat(Order/CompleteLattice): generic lemmas about membership under lattice operations~~ feat(Order/CompleteLattice): more lemmas about membership under lattice operations Sep 30, 2026

artie2000 mentioned this pull request Sep 30, 2026

chore(Order): move Order/CompleteLattice/SetLike.lean to more descriptive location #44355

Open

artie2000 added the WIP Work in progress label Sep 30, 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 Oct 9, 2026

Merge branch 'master' into setlike_lattice_lemmas

c0384d7

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 14, 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 Oct 24, 2026

Conversation

artie2000 commented Sep 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary c0384d7847

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- stale, waiting for the new build)

Uh oh!

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

Uh oh!

✅ PR Title Formatted Correctly

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!

Choose a reason for hiding this comment

Uh oh!

mathlib-dependent-issues Bot commented Sep 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

artie2000 Sep 28, 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!

artie2000 commented Sep 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-merge-conflicts Bot commented Oct 9, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Oct 24, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

artie2000 commented Sep 27, 2026 •

edited

Loading

github-actions Bot commented Sep 27, 2026 •

edited

Loading

github-actions Bot commented Sep 27, 2026 •

edited

Loading

mathlib-dependent-issues Bot commented Sep 28, 2026 •

edited

Loading

artie2000 Sep 28, 2026 •

edited

Loading

artie2000 commented Sep 30, 2026 •

edited

Loading