Commit 2022-05-22 14:41 a836c6db

refactor(category_theory): remove some simp lemmas about eq_to_hom (#14260) The simp lemma eq_to_hom_map : F.map (eq_to_hom p) = eq_to_hom (congr_arg F.obj p) is rather dangerous, but after it has fired it's much harder to see the functor F (e.g. to use naturality of a natural transformation). This PR removes @[simp] from that lemma, at the expense of having a few local attribute [simp]s, and adding it explicitly to simp sets. On the upside, we also get to remove some simp [-eq_to_hom_map]s. I'm hoping also to soon be able to remove opaque_eq_to_hom, as it was introduced to avoid the problem this simp lemma was causing. The PR is part of an effort to solve some problems identified on zulip.