Commit 2023-03-28 11:22 0148d455

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.