mathlib

0148d455 - chore(category_theory/adjunction/opposites): backport removal of simp lemmas (#18680)

chore(category_theory/adjunction/opposites): backport removal of simp lemmas (#18680) Some of the lemmas generated by `simps` in https://github.com/leanprover-community/mathlib4/pull/2424 are bad according to the simpNF linter, and have proved hard to fix by hand. Fortunately, they are simply not needed. This PR verifies this by backporting their removal to mathlib3. Compiles locally, lets hope CI agrees. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>