∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type u_3}
  [inst_2 : Fintype J] {f : J → C} (b : CategoryTheory.Limits.Bicone f),
  ∑ j, CategoryTheory.CategoryStruct.comp (b.π j) (b.ι j) = CategoryTheory.CategoryStruct.id b.pt →
    ∀ (s : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)) (m : b.toCocone.pt ⟶ s.pt),
      (∀ (j : CategoryTheory.Discrete J), CategoryTheory.CategoryStruct.comp (b.toCocone.ι.app j) m = s.ι.app j) →
        m = ∑ j, CategoryTheory.CategoryStruct.comp (b.π j) (s.ι.app { as := j })