∀ {A : Type u_6} {B : Type u_3} {C : Type u_8} [inst : CategoryTheory.Category.{u_5, u_6} A]
  [inst_1 : CategoryTheory.Category.{u_2, u_3} B] [inst_2 : CategoryTheory.Category.{u_7, u_8} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u_1)
  [inst_3 : CategoryTheory.Category.{u_4, u_1} X] (x : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight
        (CategoryTheory.NatIso.ofComponents
            (fun x_1 =>
              CategoryTheory.Iso.refl
                ((((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).comp
                            (CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X)).obj
                        x).fst.obj
                  x_1))
            ⋯).hom
        F)
      ((CategoryTheory.Functor.id (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)).obj x).iso.hom =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).comp
                (CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X)).obj
            x).iso.hom
      (CategoryTheory.Functor.whiskerRight
        (CategoryTheory.NatIso.ofComponents
            (fun x_1 =>
              CategoryTheory.Iso.refl
                ((((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).comp
                            (CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver F G X)).obj
                        x).snd.obj
                  x_1))
            ⋯).hom
        G)