∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasColimit F] {j j' : J} {x : F.obj j} (f : j ⟶ j'),
  CategoryTheory.Limits.colimit.ι F j' (F.map f x) = CategoryTheory.Limits.colimit.ι F j x