∀ {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} {A₁ : Type u_11} {B₁ : Type u_14} {C₁ : Type u_12}
  [inst_3 : CategoryTheory.Category.{u_9, u_11} A₁] [inst_4 : CategoryTheory.Category.{u_13, u_14} B₁]
  [inst_5 : CategoryTheory.Category.{u_10, u_12} C₁] {F₁ : CategoryTheory.Functor A₁ B₁}
  {G₁ : CategoryTheory.Functor C₁ B₁} (X : Type u_8) [inst_6 : CategoryTheory.Category.{u_4, u_8} X]
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X),
  { fst := CategoryTheory.Functor.whiskerRight (CategoryTheory.CategoryStruct.id X_1).fst ψ.left,
      snd := CategoryTheory.Functor.whiskerRight (CategoryTheory.CategoryStruct.id X_1).snd ψ.right, w := ⋯ } =
    CategoryTheory.CategoryStruct.id
      { fst := X_1.fst.comp ψ.left, snd := X_1.snd.comp ψ.right,
        iso :=
          X_1.fst.associator ψ.left F₁ ≪≫
            X_1.fst.isoWhiskerLeft (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
              (X_1.fst.associator F ψ.base).symm ≪≫
                CategoryTheory.Functor.isoWhiskerRight X_1.iso ψ.base ≪≫
                  X_1.snd.associator G ψ.base ≪≫
                    X_1.snd.isoWhiskerLeft (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                      (X_1.snd.associator ψ.right G₁).symm }