∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)),
  CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G =
    (CategoryTheory.preservesLimitIso ((CategoryTheory.Functor.whiskeringRight C D E).obj F) G).symm