mathlib3

8b8a5a27 - feat(category/eq_to_hom): lemmas to replace rewriting in objects with eq_to_hom (#6252)

feat(category/eq_to_hom): lemmas to replace rewriting in objects with eq_to_hom (#6252) This adds two lemmas which replace expressions in which we've used `eq.mpr` to rewrite the source or target of a morphism, replacing the `eq.mpr` by composition with an `eq_to_hom`. Possibly we just shouldn't add these Co-authored-by: Scott Morrison <scott.morrison@gmail.com>