Commit 2025-11-24 17:30 5b8332a5

feat(Category/Basic): remove simps projection Hom from CategoryStruct (#31943) This PR removes the undesirable Hom simps projection for CategoryStruct. This mainly seems to be affecting lemmas about products of categories, where prod_Hom was often used before. Fixing the errors forced me to remove many instances when the standard (non-ideal) constructor was used as opposed to Prod.mkHom. I also made the simp lemmas of prodMonoidal more consistent, it was strange that associator was a simp lemma but leftUnitor and rightUnitor were not (although one could argue that none of those three should be simp lemmas, but at least now its consistent). Doing this has lead to a general improvement (or expected behaviour of needing to replace by simp with by intros; ext; all_goals simp in one file).