∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_2, u_4} C] {D : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_5, u_6} D] (G : CategoryTheory.Functor C D) {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{u_1, u_3} J] [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape J G]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D] [inst_5 : CategoryTheory.Limits.HasLimitsOfShape J C]
  {X Y : CategoryTheory.Functor J C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.lim.comp G).map f)
      ((fun F => CategoryTheory.preservesLimitIso G F) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun F => CategoryTheory.preservesLimitIso G F) X).hom
      ((((CategoryTheory.Functor.whiskeringRight J C D).obj G).comp CategoryTheory.Limits.lim).map f)