mathlib

abf5dfca - refactor(category_theory/eq_to_hom): conjugation by eq_to_hom same as heq (#12025)

refactor(category_theory/eq_to_hom): conjugation by eq_to_hom same as heq (#12025) Xu Junyan provided this lemma for showing that `heq` gives the same as conjugation by `eq_to_hom` for equality of functor maps. I refactored `hext` using this result. Then I added a bunch of lemmas for how `heq` interacts with composition of functors and `functor.map` applied to composition of morphisms Co-authored-by: jlh <48520973+Jlh18@users.noreply.github.com>