fix after rebasing

Author: datokrat

Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean

@@ -169,9 +169,6 @@ def tensorFunc : F C ⥤ N C ⥤ F C where
 theorem tensorFunc_map_app {X Y : F C} (f : X ⟶ Y) (n) : ((tensorFunc C).map f).app n = _ ◁ f :=
   rfl
 
-set_option allowUnsafeReducibility true
-attribute [implicit_reducible] Pi.instCategoryComp._aux_1
-
 theorem tensorFunc_obj_map (Z : F C) {n n' : N C} (f : n ⟶ n') :
     ((tensorFunc C).obj Z).map f = inclusion.map f ▷ Z := by
   cases n

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c07adf1a2e4448217e14428328d34c9c1501dcec",
+   "rev": "e4a9b9107417982d95052a056416cf891355df66",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "lean-pr-testing-13342",