∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) {j j' : J}
  (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (F.map f) (CommRingCat.Colimits.coconeMorphism F j') =
    CommRingCat.Colimits.coconeMorphism F j