∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G) (j : J) {Z : C}
  (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).inv
      (CategoryTheory.CategoryStruct.comp (s.π.app j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (t.π.app j) (w.inv.app j)) h