∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {ι₁ : Type u_1} {ι₂ : Type u_2} {f₁ : ι₁ → C}
  {f₂ : ι₂ → C} {c₁ : CategoryTheory.Limits.Cofan f₁} {c₂ : CategoryTheory.Limits.Cofan f₂}
  {bc : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt} (h₁ : CategoryTheory.Limits.IsColimit c₁)
  (h₂ : CategoryTheory.Limits.IsColimit c₂) (h : CategoryTheory.Limits.IsColimit bc)
  (s : CategoryTheory.Limits.Cofan (Sum.elim f₁ f₂))
  (m : (CategoryTheory.Limits.Cofan.mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt),
  (∀ (j : ι₁ ⊕ ι₂),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Cofan.mk bc.pt (c₁.combPairHoms c₂ bc)).inj j) m =
        s.inj j) →
    m =
      CategoryTheory.Limits.Cofan.IsColimit.desc h fun i =>
        CategoryTheory.Limits.WalkingPair.casesOn (motive := fun t =>
          i = t → (CategoryTheory.Limits.WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h => ⋯ ▸ CategoryTheory.Limits.Cofan.IsColimit.desc h₁ fun a => s.inj (Sum.inl a))
          (fun h => ⋯ ▸ CategoryTheory.Limits.Cofan.IsColimit.desc h₂ fun a => s.inj (Sum.inr a)) ⋯