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

leanprover-community · Aug 19, 2019 · 5a309a3 · 5a309a3
1 parent 9eefd40
commit 5a309a3
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/category_theory/eq_to_hom.lean b/src/category_theory/eq_to_hom.lean
@@ -70,15 +70,15 @@ by subst h; simp
 
 end functor
 
-@[simp] lemma eq_to_hom_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
+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
 
-@[simp] lemma eq_to_iso_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
+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
 
-@[simp] lemma eq_to_hom_app {F G : C ⥤ D} (h : F = G) (X : C) :
+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