[Merged by Bors] - chore(Data/Set/Card): make s.ncard the simpNF of Fintype.card s#39414
Closed
SnirBroshi wants to merge 2 commits into
Closed
[Merged by Bors] - chore(Data/Set/Card): make s.ncard the simpNF of Fintype.card s#39414SnirBroshi wants to merge 2 commits into
s.ncard the simpNF of Fintype.card s#39414SnirBroshi wants to merge 2 commits into
Conversation
PR summary a5c1b3289aImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
b-mehta
reviewed
May 18, 2026
Comment on lines
+333
to
335
| @[to_dual self] | ||
| theorem _root_.Fintype.card_Icc (a b : α) [Fintype (Set.Icc a b)] : | ||
| Fintype.card (Set.Icc a b) = #(Icc a b) := |
Contributor
There was a problem hiding this comment.
Can simp now prove these lemmas (in a different way)?
Collaborator
Author
There was a problem hiding this comment.
No, it just simplifies the LHS to Set.ncard (after Mathlib/Data/Set/Card.lean, not here) so simpNF is angry.
I also think these are pretty strange as simp lemmas, but maybe I haven't used LocallyFiniteOrder enough to see its value.
Contributor
There was a problem hiding this comment.
These lemmas should be stated in terms of Set.ncard. They were written before the definition existed
Contributor
There was a problem hiding this comment.
Can you make a follow-up PR to make this change?
YaelDillies
approved these changes
May 21, 2026
mathlib-bors Bot
pushed a commit
that referenced
this pull request
May 24, 2026
…39414) Untags `coe_fintypeCard : ↑(Fintype.card s) = s.encard` as `@[simp]`, and instead tags - `fintypeCard_eq_ncard : Fintype.card s = s.ncard` - `coe_ncard_eq_encard : ↑(s.ncard) = s.encard` Then untags `simp` lemmas which are no longer simpNF because of this change; simpNF versions of some of them will be introduced in future PRs.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
Bot
changed the title
s.ncard the simpNF of Fintype.card ss.ncard the simpNF of Fintype.card s
b-mehta
pushed a commit
to b-mehta/mathlib4
that referenced
this pull request
Jun 2, 2026
…eanprover-community#39414) Untags `coe_fintypeCard : ↑(Fintype.card s) = s.encard` as `@[simp]`, and instead tags - `fintypeCard_eq_ncard : Fintype.card s = s.ncard` - `coe_ncard_eq_encard : ↑(s.ncard) = s.encard` Then untags `simp` lemmas which are no longer simpNF because of this change; simpNF versions of some of them will be introduced in future PRs.
Bergschaf
pushed a commit
to Bergschaf/mathlib4
that referenced
this pull request
Jun 3, 2026
…eanprover-community#39414) Untags `coe_fintypeCard : ↑(Fintype.card s) = s.encard` as `@[simp]`, and instead tags - `fintypeCard_eq_ncard : Fintype.card s = s.ncard` - `coe_ncard_eq_encard : ↑(s.ncard) = s.encard` Then untags `simp` lemmas which are no longer simpNF because of this change; simpNF versions of some of them will be introduced in future PRs.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Untags
coe_fintypeCard : ↑(Fintype.card s) = s.encardas@[simp], and instead tagsfintypeCard_eq_ncard : Fintype.card s = s.ncardcoe_ncard_eq_encard : ↑(s.ncard) = s.encardThen untags
simplemmas which are no longer simpNF because of this change;simpNF versions of some of them will be introduced in future PRs.