∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {α : Type u_3}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] (I : Finset (CategoryTheory.Discrete α))
  {X Y : CategoryTheory.Functor (CategoryTheory.Discrete α) C} (x : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).comp
            ((CategoryTheory.evaluation (Finset (CategoryTheory.Discrete α)) C).obj I)).map
        x)
      ((fun x =>
            CategoryTheory.Limits.HasColimit.isoOfNatIso
              (CategoryTheory.Discrete.natIso fun x_1 =>
                CategoryTheory.Iso.refl ((CategoryTheory.Discrete.functor fun x_2 => x.obj ↑x_2).obj x_1)))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            CategoryTheory.Limits.HasColimit.isoOfNatIso
              (CategoryTheory.Discrete.natIso fun x_1 =>
                CategoryTheory.Iso.refl ((CategoryTheory.Discrete.functor fun x_2 => x.obj ↑x_2).obj x_1)))
          X).hom
      ((((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete ↥I) (CategoryTheory.Discrete α) C).obj
                (CategoryTheory.Discrete.functor fun x => ↑x)).comp
            CategoryTheory.Limits.colim).map
        x)