∀ {C : Type u_5} [inst : CategoryTheory.Category.{u_4, u_5} C] {A : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_2, u_3} A] [inst_2 : CategoryTheory.Limits.HasCoproducts A] (J : Type u_1)
  (f : J → CategoryTheory.Limits.FormalCoproduct C) (F : CategoryTheory.Functor C A)
  (s :
    CategoryTheory.Limits.Cocone
      ((CategoryTheory.Discrete.functor f).comp ((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F)))
  (m :
    (((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F).mapCocone
          (CategoryTheory.Limits.FormalCoproduct.cofan J f)).pt ⟶
      s.pt),
  (∀ (j : CategoryTheory.Discrete J),
      CategoryTheory.CategoryStruct.comp
          ((((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F).mapCocone
                  (CategoryTheory.Limits.FormalCoproduct.cofan J f)).ι.app
            j)
          m =
        s.ι.app j) →
    m =
      CategoryTheory.Limits.Sigma.desc fun i =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (F.obj ∘ (f i.fst).obj) i.snd)
          (s.ι.app { as := i.fst })