∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) (α : Type t)
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C],
  CategoryTheory.Limits.FormalCoproduct.powerMap (CategoryTheory.CategoryStruct.id U) α =
    CategoryTheory.CategoryStruct.id (U.power α)