∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D) (s : α) {Z : C} (h : (f s).obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piObjIso f d).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun s => (f s).obj d) s) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.Pi.π f s).app d) h