∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (X : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X_1 : K),
  (CategoryTheory.Limits.limCompFlipIsoWhiskerLim.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation X X_1)).inv
      (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation X.flip X_1).inv