∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (c : CategoryTheory.Limits.Cowedge F) {i j : J}
  (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app i) (CategoryTheory.Limits.Multicofork.π c i) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (CategoryTheory.Limits.Multicofork.π c j)