mathlib3

a836c6db - refactor(category_theory): remove some simp lemmas about eq_to_hom (#14260)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/trouble.20in.20.60shift_functor.60.20land). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>