[Merged by Bors] - feat(Fintype.Basic): Add two theorems supporting Auction Theory formalizations

[hcWang942]

This PR adds two missing theorems in Mathlib.Data.Fintype.Basic

---

This is used in another PR of mine formalizing some basic theorems in GameTheory.AuctionTheory.Basic .

One may check the previous PR for Auction Theory here: #13248

I would sincerely appreciate a timely review of this PR, as I am eager to complete my first project on Auction Theory before my upcoming birthday. Thank you very much for your consideration and support!

[github-actions]

PR summary 64a9375e03

Import changes

No significant changes to the import graph

---

Declarations diff

+ univ_nontrivial
+ univ_nontrivial_iff:

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>

[Shreyas4991]

It seems you have rebased your PR on the other PR branch so now we have all these other commits which are not needed in this PR. In your branch finset_nontrivial_two_theorems_add can you remove those commits by resetting HEAD to the latest master commit and then commit only the two new theorems? Once you only have the one new commit in this branch for adding the two theorems, you will have to force push to this branch here.

[hcWang942]

May I know if it is correct to use the command
`
git fetch origin master

git reset --hard origin/master
`
Then commit and push the changes again. I find there is nothing changed after applying the above command. Can you please give me some suggestion?

[Shreyas4991]

You don't need to git fetch origin master. I have a beginner friendly but slightly tedious idea. I am assuming you are currently on this branch at the last I commit I see on this page 9659d19. if you open git log by running git log and scroll down, you will find the most recent commit that is not your commit in this PR. copy that commit ID (which I denote by <commit_ID> hereon). then git reset --hard <commit_ID>. Then add your two theorems (which you can in the respective file). add and commit that. Then git push --force origin finset_nontrivial_two_theorems_add

I am so so sorry. Instead of hitting reply, I seem to have hit edit on your comment. I hope the question you have was answered though. I have restored your version of the comment. You can find my response quoted above.

[Shreyas4991]

Could you please delete this file https://github.com/leanprover-community/mathlib4/pull/14163/files#diff-ffd24c8f58ab0af7a8d4610ab7fc208cf0fef60e76059dcd605f7113179a96ca

EDIT: You can do this from this webpage by going to the files changed tab at the top your PR description and deleting that large file with 66000 changes.

EDIT 2 : If I have to guess the cause of this file, git probably opened your text editor for the commit message after the reset and for reasons beyond me saved the file into the toplevel directory of your local clone of mathlib. This file can be safely discarded.

[hcWang942]

Could you please delete this file https://github.com/leanprover-community/mathlib4/pull/14163/files#diff-ffd24c8f58ab0af7a8d4610ab7fc208cf0fef60e76059dcd605f7113179a96ca

EDIT: You can do this from this webpage by going to the files changed tab at the top your PR description and deleting that large file with 66000 changes.

EDIT 2 : If I have to guess the cause of this file, git probably opened your text editor for the commit message after the reset and for reasons beyond me saved the file into the toplevel directory of your local clone of mathlib. This file can be safely discarded.

Thanks for the suggestion, relevant modification has been done!

[Shreyas4991]

I am not convinced that univ_nontrivial belongs in mathlib. I don't think it is mathlib practice to have mp and mpr versions of lemmas as separate globally named lemmas. The iff version suffices. univ_nontrivial_iff can be used with rw and univ_nontrivial_iff.mpr with apply, depending on which tactic you are using.

[tb65536]

The one advantage of univ_nontrivial is that it can take Nontrivial α automatically. For instance, see univ_nonempty_iff and univ_nonempty a few lines above.

[Shreyas4991]

The one advantage of univ_nontrivial is that it can take Nontrivial α automatically. For instance, see univ_nonempty_iff and univ_nonempty a few lines above.

If so, is there a reason this theorem is not an instance declaration instead?

[tb65536]

The one advantage of univ_nontrivial is that it can take Nontrivial α automatically. For instance, see univ_nonempty_iff and univ_nonempty a few lines above.

If so, is there a reason this theorem is not an instance declaration instead?

I think Finset.Nonempty and Finset.Nontrivial are just defs, not typeclasses.

[Shreyas4991]

The one advantage of univ_nontrivial is that it can take Nontrivial α automatically. For instance, see univ_nonempty_iff and univ_nonempty a few lines above.

If so, is there a reason this theorem is not an instance declaration instead?

I think Finset.Nonempty and Finset.Nontrivial are just defs, not typeclasses.

Okay then I take back that comment, but I still don't see why univ_nonempty_iff.mpr is not giving you the same ease of use as univ_nonempty. That being said, I am not an official reviewer or maintainer, so please take this opinion with a pinch of salt.

[tb65536]

I think the above discussion has resolved and this is still waiting for review? Personally, this PR looks good to me.

[hcWang942]

I think the above discussion has resolved and this is still waiting for review? Personally, this PR looks good to me.

Thanks for the kind reply, may I know what more can I do now? Or I just need to wait patiently.

[j-loreaux]

Arguably, Finset.univ_nontrivial could / should be marked @[simp], but I think I prefer it as is so that we don't insert this generic typeclass search into the simp calls.

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style