Revert "fix(category_theory/eq_to_hom): remove bad simp lemmas (#1346)…

…" (#2713)

These are good simp lemmas: they push things into a proof-irrelevant position.

This reverts commit 5a309a3.

src/category_theory/eq_to_hom.lean

@@ -67,15 +67,15 @@ by subst h; simp
 
 end functor
 
-lemma eq_to_hom_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
+@[simp] lemma eq_to_hom_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
   F.map (eq_to_hom p) = eq_to_hom (congr_arg F.obj p) :=
 by cases p; simp
 
-lemma eq_to_iso_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
+@[simp] lemma eq_to_iso_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
   F.map_iso (eq_to_iso p) = eq_to_iso (congr_arg F.obj p) :=
 by ext; cases p; simp
 
-lemma eq_to_hom_app {F G : C ⥤ D} (h : F = G) (X : C) :
+@[simp] lemma eq_to_hom_app {F G : C ⥤ D} (h : F = G) (X : C) :
   (eq_to_hom h : F ⟶ G).app X = eq_to_hom (functor.congr_obj h X) :=
 by subst h; refl