chore(category_theory/functor): make arguments implicit (#2103)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
leanprover-community · Mar 8, 2020 · 15d3268 · 15d3268
1 parent b7444b0
commit 15d3268
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/category_theory/functor.lean b/src/category_theory/functor.lean
@@ -78,7 +78,7 @@ def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E :=
 infixr ` ⋙ `:80 := comp
 
 @[simp] lemma comp_obj (F : C ⥤ D) (G : D ⥤ E) (X : C) : (F ⋙ G).obj X = G.obj (F.obj X) := rfl
-@[simp] lemma comp_map (F : C ⥤ D) (G : D ⥤ E) (X Y : C) (f : X ⟶ Y) :
+@[simp] lemma comp_map (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) :
   (F ⋙ G).map f = G.map (F.map f) := rfl
 
 omit ℰ