∀ {A : Type u_4} {B : Type u_2} {C : Type u_6} [inst : CategoryTheory.Category.{u_3, u_4} A]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} B] [inst_2 : CategoryTheory.Category.{u_5, u_6} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u_8)
  [inst_3 : CategoryTheory.Category.{u_7, u_8} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (φ : S ⟶ S') (x : X),
  CategoryTheory.CategoryStruct.comp (F.map (φ.fst.app x))
      ({ obj := fun x => { fst := S'.fst.obj x, snd := S'.snd.obj x, iso := S'.iso.app x },
                map := fun {x y} f => { fst := S'.fst.map f, snd := S'.snd.map f, w := ⋯ }, map_id := ⋯,
                map_comp := ⋯ }.obj
            x).iso.hom =
    CategoryTheory.CategoryStruct.comp
      ({ obj := fun x => { fst := S.fst.obj x, snd := S.snd.obj x, iso := S.iso.app x },
                map := fun {x y} f => { fst := S.fst.map f, snd := S.snd.map f, w := ⋯ }, map_id := ⋯,
                map_comp := ⋯ }.obj
            x).iso.hom
      (G.map (φ.snd.app x))