∀ {A : Type u_5} {B : Type u_6} {C : Type u_7} [inst : CategoryTheory.Category.{u_1, u_5} A]
  [inst_1 : CategoryTheory.Category.{u_2, u_6} B] [inst_2 : CategoryTheory.Category.{u_3, u_7} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u_8)
  [inst_3 : CategoryTheory.Category.{u_4, u_8} X]
  {X_1 Y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X} (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.fstFunctor F G X).comp
            ((CategoryTheory.Functor.whiskeringRight X A B).obj F)).map
        f)
      ((fun S => S.iso) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun S => S.iso) X_1).hom
      (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor F G X).comp
            ((CategoryTheory.Functor.whiskeringRight X C B).obj G)).map
        f)