∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C}
  (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl))
  (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c)
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  [CategoryTheory.Limits.MonoCoprod C] (inr : c₂.pt ⟶ c.pt),
  (∀ (i₂ : I₂), CategoryTheory.CategoryStruct.comp (c₂.inj i₂) inr = c.inj (Sum.inr i₂)) → CategoryTheory.Mono inr