feat(push): @[push] attributes for ∈ in Set, Finset and Multiset#30042
feat(push): @[push] attributes for ∈ in Set, Finset and Multiset#30042JovanGerb wants to merge 6 commits intoleanprover-community:masterfrom
@[push] attributes for ∈ in Set, Finset and Multiset#30042Conversation
PR summary 29d85a079c
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Order.Interval.Set.Defs | 64 | 65 | +1 (+1.56%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Order.Interval.Set.Defs |
1 |
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
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
This pull request has conflicts, please merge |
|
This pull request has conflicts, please merge |
|
This pull request has conflicts, please merge |
grunweg
left a comment
There was a problem hiding this comment.
Thanks! I have a few minor comments and a few requests for a few more tests. Getting this used to golf mathlib would be nice - but that can happen in a future PR.
| end lambda | ||
|
|
||
| section membership | ||
|
|
There was a problem hiding this comment.
Can you add some tests for intervals also?
| @@ -68,7 +69,7 @@ variable {α : Type u} {β : Type v} {γ : Type w} | |||
|
|
|||
| /-! ### Lemmas about `mem` and `setOf` -/ | |||
|
|
|||
There was a problem hiding this comment.
Can you add a few basic tests for this file? Say, for mem_setOf, mem_univ or mem_range?
| alias eq_of_not_mem_of_mem_insert := eq_of_mem_insert_of_notMem | ||
|
|
||
| @[simp, grind =] | ||
| @[simp, grind =, push] |
There was a problem hiding this comment.
A test for this or mem_singleton_iff would be nice.
| exact ⟨fun i ↦ _, rfl⟩ | ||
|
|
||
| @[to_additive] | ||
| @[to_additive (attr := push)] |
There was a problem hiding this comment.
This is probably not a good simp lemma, but might be a fine push lemma.
| · intro i s _ ih | ||
| rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih] | ||
|
|
||
| @[push] |
There was a problem hiding this comment.
I don't know why this lemma is not simp, but Finset.mem_sup` is. Oh well...
| by rw [eq] | ||
| neb <| show b₁ = b₂ by rwa [Pi.cons_same, Pi.cons_same] at this) | ||
|
|
||
| @[push] |
There was a problem hiding this comment.
This would be a terrible simp lemma. I'm not sure if it would be a good push lemma - but if this only fires on a hypothesis f \in pi m t, perhaps it's fine?
|
This pull request has conflicts, please merge |
This PR adds `@[push]` tags for set membership. This is a subset of leanprover-community#30042, namely all the `Set` tags. leanprover-community#30042 also has tags for `Finset` and `Multiset`; as `Set` is the biggest use case of these, we start with just these.
This PR adds `@[push]` tags for set membership. This is a subset of leanprover-community#30042, namely all the `Set` tags. leanprover-community#30042 also has tags for `Finset` and `Multiset`; as `Set` is the biggest use case of these, we start with just these.
This PR adds `@[push]` tags for set membership. This is a subset of leanprover-community#30042, namely all the `Set` tags. leanprover-community#30042 also has tags for `Finset` and `Multiset`; as `Set` is the biggest use case of these, we start with just these.
This PR adds
@[push]annotations for the membership relations, forSet,FinsetandMultiset.