∀ {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.HasProducts A] (J : Type u_1)
  (f : J → CategoryTheory.Limits.FormalCoproduct C) (F : CategoryTheory.Functor Cᵒᵖ A)
  (s :
    CategoryTheory.Limits.Cone
      ((CategoryTheory.Discrete.functor fun x => Opposite.op (f x)).comp
        ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F)))
  (m :
    s.pt ⟶
      (((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F).mapCone
          (CategoryTheory.Limits.FormalCoproduct.cofan J f).op).pt),
  (∀ (j : CategoryTheory.Discrete J),
      CategoryTheory.CategoryStruct.comp m
          ((((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F).mapCone
                  (CategoryTheory.Limits.FormalCoproduct.cofan J f).op).π.app
            j) =
        s.π.app j) →
    m =
      CategoryTheory.Limits.Pi.lift fun i =>
        CategoryTheory.CategoryStruct.comp (s.π.app { as := i.fst })
          (CategoryTheory.Limits.Pi.π
            (fun i_1 =>
              F.obj
                (Opposite.op
                  ((Opposite.unop
                        ((CategoryTheory.Discrete.functor fun x => Opposite.op (f x)).obj { as := i.fst })).obj
                    i_1)))
            i.snd)