Commit 2025-02-23 19:55 a10773c2

chore(CategoryTheory): turn more simp into simps! (#22223) Turn some possibly mistaken simp attributes on definitions of isomorphisms into simps. In some cases, the projections were already recorded as simp lemmas, so the attribute was simply removed. Note: as it seems some things were relying on the definitional properties of Functor.mapBiprod and Functor.mapBiproduct, removing their simp attribute require turning them into abbrev.