Commit 2024-05-30 08:29 6d39f512

chore(Category/TopCat): cleanup (#13170) This PR removes an instance (ConcreteCategory.instFunLike) that was mistakenly made global during the port and starts the clean up. It significantly speeds up CI since simp is more efficient. Unfortunately, some simp's and rw's needed to be changed to erw as a result. Zulip discussion: #mathlib4 > ConcreteCategory.instFunLike became a global instance Issue: #13342