[Merged by Bors] - feat: more lemmas about List.dedup and other lattice operations#14282
[Merged by Bors] - feat: more lemmas about List.dedup and other lattice operations#14282eric-wieser wants to merge 16 commits intomasterfrom
List.dedup and other lattice operations#14282Conversation
PR summary 179ad54926
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.List.Dedup | 324 | 325 | +1 (+0.31%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Data.List.Dedup |
1 |
Declarations diff
+ Disjoint.dedup_add
+ Disjoint.dedup_append
+ Disjoint.inter_eq_nil
+ Disjoint.ndinter_eq_zero
+ Disjoint.ndunion_eq
+ Disjoint.union_eq
+ Subset.dedup_add_left
+ Subset.dedup_add_right
+ Subset.dedup_append_right
+ Subset.inter_eq_left
+ Subset.ndinter_eq_left
+ Subset.ndunion_eq_right
+ Subset.union_eq_right
+ _root_.List.Subset.dedup_append_left
+ inter_nil'
++ _
++ dedup_map_of_injective
You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>|
|
||
| theorem dedup_map_of_injective [DecidableEq β] {f : α → β} (hf : Function.Injective f) | ||
| (xs : List α) : | ||
| (xs.map f).dedup = xs.dedup.map f := by |
There was a problem hiding this comment.
@Timeroot had this lemma somewhere. Did it ever land? What is the PR?
There was a problem hiding this comment.
I assume we don't need to wait for an answer here? Of course, if @Timeroot comes along with a shorter proof after this is merged, we can always make a golf PR.
|
|
||
| alias ⟨_, Disjoint.ndinter_eq_zero⟩ := ndinter_eq_zero_iff_disjoint | ||
|
|
||
| theorem Subset.ndinter_eq_left {s t : Multiset α} (h : s ⊆ t) : s.ndinter t = s := by |
There was a problem hiding this comment.
Same, can we have the right verSion?
There was a problem hiding this comment.
I don't think the right version is meaningfully true? What statement do you want?
There was a problem hiding this comment.
Ah indeed. But then this lemma is something like Multiset.filter_true_of_mem h except that filter_true_of_mem doesn't exist
There was a problem hiding this comment.
It exists for List though; I golfed the proof there
YaelDillies
left a comment
There was a problem hiding this comment.
Looks good now
maintainer merge
|
maintainer merge The conspiracy for bots to ignore Yael continues |
|
🚀 Pull request has been placed on the maintainer queue by eric-wieser. |
|
!bench |
|
I would guess the import change and the single simp are good but benched so I don't have to speculate. If it comes back reasonable, please merge. Thanks! bors delegate+ |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Here are the benchmark results for commit 179ad54. |
|
bors r+ |
…4282) Also the trivial `Multiset` wrappers.
|
Pull request successfully merged into master. Build succeeded: |
List.dedup and other lattice operationsList.dedup and other lattice operations
Also the trivial
Multisetwrappers.