chore(category_theory/opposites): make hom explicit in lemmas (#8088)

Author: jcommelin

src/algebraic_topology/simplicial_object.lean

@@ -246,7 +246,7 @@ def augment (X : simplicial_object C) (X₀ : C) (f : X _[0] ⟶ X₀)
     naturality' := begin
       intros i j g,
       dsimp,
-      rw ← (quiver.hom.op_unop : g.unop.op = g),
+      rw ← g.op_unop,
       simpa only [← X.map_comp, ← category.assoc, category.comp_id, ← op_comp] using w _ _ _,
     end } }
 

src/category_theory/opposites.lean

@@ -24,8 +24,8 @@ lemma quiver.hom.unop_inj {X Y : Cᵒᵖ} :
   function.injective (quiver.hom.unop : (X ⟶ Y) → (unop Y ⟶ unop X)) :=
 λ _ _ H, congr_arg quiver.hom.op H
 
-@[simp] lemma quiver.hom.unop_op {X Y : C} {f : X ⟶ Y} : f.op.unop = f := rfl
-@[simp] lemma quiver.hom.op_unop {X Y : Cᵒᵖ} {f : X ⟶ Y} : f.unop.op = f := rfl
+@[simp] lemma quiver.hom.unop_op {X Y : C} (f : X ⟶ Y) : f.op.unop = f := rfl
+@[simp] lemma quiver.hom.op_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) : f.unop.op = f := rfl
 
 end quiver