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](https://github.com/leanprover-community/mathlib/tree/alexjbest/simple_edge_cases_linter?rgh-link-date=2021-12-13T23%3A53%3A31Z)
