PR summary 64a9375e03

Import changes

No significant changes to the import graph

Declarations diff

+ univ_nontrivial
+ univ_nontrivial_iff:

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

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.

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?

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.

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.

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!

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.

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?

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.

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.

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.

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

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style