Commit 2022-04-11 20:58 4a070542

chore(*): remove numerous edge cases from lemmas (#13316) This PR uses the same methodology as #10774 to use a linter to remove edge case assumptions from lemmas when the result is easy to prove without the assumption. These are assumptions things like: n \ne 0, 0 < n, p \ne \top, nontrivial R, nonempty R. Removing these unneeded assumptions makes such lemmas easier to apply, and lets us golf a few other proofs along the way. The file with the most changes is src/ring_theory/unique_factorization_domain.lean where the linter inspired me to allow trivial monoids in many places. The code I used to find these is in the branch https://github.com/leanprover-community/mathlib/tree/alexjbest/simple_edge_cases_linter