Adding a useful massing lemma: `not_mem_singleton_iff`

[sinhp]

The contrapositive (?) of the lemma

theorem mem_singleton_iff {a b : α} : a ∈ ({b} : Set α) ↔ a = b :=
  Iff.rfl

was missing. This PR adds

@[simp]
theorem not_mem_singleton_iff {a b : α} : a ∉ ({b} : Set α) ↔ a ≠ b :=
  Iff.rfl

which can be useful in avoiding extra have statements in other proofs.

---

[github-actions[bot]]

PR summary 371bc73f7f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ not_mem_singleton_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>

[dagurtomas]

This PR includes some Grothendieck construction stuff, which it shouldn't, according to the PR description

[sinhp]

This PR includes some Grothendieck construction stuff, which it shouldn't, according to the PR description

So, I think this is because I am doing something wrong: I have only one mathlib repo locally, and do all my PRs from that. I do follow the Mathlib contribution guidelines in switching branches first, but nevertheless I get the problem that this PR for sets shows up as a continuation of GrothendieckIsFunctorial branch. What am I missing?

[erdOne]

git checkout master Mathlib/CategoryTheory/Grothendieck.lean on that branch will reset the file to master. Be sure to back up first!

[sinhp]

git checkout master Mathlib/CategoryTheory/Grothendieck.lean on that branch will reset the file to master. Be sure to back up first!

Just did that. Would the next step be for the current PR (i.e. not_mem_singleton_iff) be to commit the change (i.e. resetting Grothendieck.lean back to the master version) and push?

[erdOne]

Yes.

[erdOne]

Thanks! maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style