∀ {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_9} {Y : Type u_8}
  [inst_3 : CategoryTheory.Category.{u_10, u_9} X] [inst_4 : CategoryTheory.Category.{u_4, u_8} Y]
  (U : CategoryTheory.Functor X Y) (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y),
  { fst := U.whiskerLeft (CategoryTheory.CategoryStruct.id X_1).fst,
      snd := U.whiskerLeft (CategoryTheory.CategoryStruct.id X_1).snd, w := ⋯ } =
    CategoryTheory.CategoryStruct.id
      { fst := U.comp X_1.fst, snd := U.comp X_1.snd,
        iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd G).symm }