mathlib

2efd2423 - chore(category_theory): simps should not add hom lemmas (#18742)

chore(category_theory): simps should not add hom lemmas (#18742) `@[simps]` should not be used to simplify the `hom` field of a category instance. Very little needs to be changed when removing it. However the problem in https://github.com/leanprover-community/mathlib4/pull/3244 with a proof by `simp` failing seems to be implicated by this problem. If we remove the `@[simps]` generated lemma for `Hom` there, the original proof works (although is extremely slow). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>