Commit 2021-12-15 19:58 75b4e5f5

chore(*): remove edge case assumptions from lemmas (#10774) Remove edge case assumptions from lemmas when the result is easy to prove without the assumption. We clean up a few lemmas in the library which assume something like n \ne 0, 0 < n, or set.nonempty but where the result is easy to prove by case splitting on this instead and then simplifying. Removing these unneeded assumptions makes such lemmas easier to apply, and lets us minorly golf a few other proofs along the way. The main external changes are to remove assumptions to around 30 lemmas, and make some arguments explicit when they were no longer inferable, all other lines are just fixing up the proofs, which shortens some proofs in the process. I also added a couple of lemmas to help simp in a couple of examples. The code I used to find these is in the branch https://github.com/leanprover-community/mathlib/tree/alexjbest/simple_edge_cases_linter