∀ (C : Type u_3) [inst : CategoryTheory.Category.{u_1, u_3} C] (A : Type u_4)
  [inst_1 : CategoryTheory.Category.{u_2, u_4} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Limits.FormalCoproduct.evalOp C A).comp
            ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ A).obj
              (CategoryTheory.Limits.FormalCoproduct.incl C).op)).map
        f)
      ((fun F =>
            CategoryTheory.NatIso.ofComponents
              (fun x =>
                {
                  hom :=
                    CategoryTheory.Limits.Pi.π
                      (fun i =>
                        F.obj
                          (Opposite.op
                            ((Opposite.unop ((CategoryTheory.Limits.FormalCoproduct.incl C).op.obj x)).obj i)))
                      PUnit.unit,
                  inv :=
                    CategoryTheory.Limits.Pi.lift fun x_1 =>
                      CategoryTheory.CategoryStruct.id
                        (((CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ A)).obj F).obj x),
                  hom_inv_id := ⋯, inv_hom_id := ⋯ })
              ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun F =>
            CategoryTheory.NatIso.ofComponents
              (fun x =>
                {
                  hom :=
                    CategoryTheory.Limits.Pi.π
                      (fun i =>
                        F.obj
                          (Opposite.op
                            ((Opposite.unop ((CategoryTheory.Limits.FormalCoproduct.incl C).op.obj x)).obj i)))
                      PUnit.unit,
                  inv :=
                    CategoryTheory.Limits.Pi.lift fun x_1 =>
                      CategoryTheory.CategoryStruct.id
                        (((CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ A)).obj F).obj x),
                  hom_inv_id := ⋯, inv_hom_id := ⋯ })
              ⋯)
          X).hom
      ((CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ A)).map f)