∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.Limits.colim.PreservesMonomorphisms]
  {X₁ X₂ : CategoryTheory.Functor J C} (φ : X₁ ⟶ X₂) [CategoryTheory.Mono φ] {c₁ : CategoryTheory.Limits.Cocone X₁}
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) {c₂ : CategoryTheory.Limits.Cocone X₂}
  (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f = CategoryTheory.CategoryStruct.comp (φ.app j) (c₂.ι.app j)) →
    CategoryTheory.Mono f