-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst_3 : Category.{v₄, u₄} A₁
inst_4 : Category.{v₅, u₅} B₁
inst_5 : Category.{v₆, u₆} C₁
F₁ : Functor.{v₄, v₅, u₄, u₅} A₁ B₁
G₁ : Functor.{v₆, v₅, u₆, u₅} C₁ B₁
X : Type u₇
inst_6 : Category.{v₇, u₇} X
X_1 : CatCospanTransform F G F₁ G₁
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) (x_1 : X),
    (NatTrans.app
              {
                app := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                  {
                    fst :=
                      { app := fun (y : X) ↦ (CatCospanTransformMorphism.left (𝟙 X_1)).app (S.fst.obj y),
                        naturality := ⋯ :
                        NatTrans.{v₇, v₄, u₇, u₄} (C := X) (D := A₁)
                          (fst.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (B := B₁) (C := C₁) (F := F₁) (G := G₁)
                            ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                                { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                                  iso :=
                                    S.fst.associator X_1.left F₁ ≪≫
                                      S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                        (S.fst.associator F X_1.base).symm ≪≫
                                          isoWhiskerRight S.iso X_1.base ≪≫
                                            S.snd.associator G X_1.base ≪≫
                                              S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                                (S.snd.associator X_1.right G₁).symm :
                                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                              S))
                          (fst.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (B := B₁) (C := C₁) (F := F₁) (G := G₁)
                            ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                                { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                                  iso :=
                                    S.fst.associator X_1.left F₁ ≪≫
                                      S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                        (S.fst.associator F X_1.base).symm ≪≫
                                          isoWhiskerRight S.iso X_1.base ≪≫
                                            S.snd.associator G X_1.base ≪≫
                                              S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                                (S.snd.associator X_1.right G₁).symm :
                                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                              S)) },
                    snd :=
                      { app := fun (y : X) ↦ (CatCospanTransformMorphism.right (𝟙 X_1)).app (S.snd.obj y),
                        naturality := ⋯ :
                        NatTrans.{v₇, v₆, u₇, u₆} (C := X) (D := C₁)
                          (snd.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (A := A₁) (B := B₁) (F := F₁) (G := G₁)
                            ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                                { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                                  iso :=
                                    S.fst.associator X_1.left F₁ ≪≫
                                      S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                        (S.fst.associator F X_1.base).symm ≪≫
                                          isoWhiskerRight S.iso X_1.base ≪≫
                                            S.snd.associator G X_1.base ≪≫
                                              S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                                (S.snd.associator X_1.right G₁).symm :
                                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                              S))
                          (snd.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (A := A₁) (B := B₁) (F := F₁) (G := G₁)
                            ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                                { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                                  iso :=
                                    S.fst.associator X_1.left F₁ ≪≫
                                      S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                        (S.fst.associator F X_1.base).symm ≪≫
                                          isoWhiskerRight S.iso X_1.base ≪≫
                                            S.snd.associator G X_1.base ≪≫
                                              S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                                (S.snd.associator X_1.right G₁).symm :
                                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                              S)) },
                    w := ⋯ :
                    Hom.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (A := A₁) (B := B₁) (C := C₁) (F := F₁) (G := G₁) X
                      ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                          { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                            iso :=
                              S.fst.associator X_1.left F₁ ≪≫
                                S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (S.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight S.iso X_1.base ≪≫
                                      S.snd.associator G X_1.base ≪≫
                                        S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (S.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                        S)
                      ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                          { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                            iso :=
                              S.fst.associator X_1.left F₁ ≪≫
                                S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (S.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight S.iso X_1.base ≪≫
                                      S.snd.associator G X_1.base ≪≫
                                        S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (S.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                        S) },
                naturality := ⋯ :
                NatTrans (C := CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) (D :=
                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X)
                  {
                    obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                      { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                        iso :=
                          S.fst.associator X_1.left F₁ ≪≫
                            S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                              (S.fst.associator F X_1.base).symm ≪≫
                                isoWhiskerRight S.iso X_1.base ≪≫
                                  S.snd.associator G X_1.base ≪≫
                                    S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                      (S.snd.associator X_1.right G₁).symm :
                        CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X },
                    map := fun {x y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X} (f : x ⟶ y) ↦
                      { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ :
                        Hom X
                          { fst := x.fst ⋙ X_1.left, snd := x.snd ⋙ X_1.right,
                            iso :=
                              x.fst.associator X_1.left F₁ ≪≫
                                x.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (x.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight x.iso X_1.base ≪≫
                                      x.snd.associator G X_1.base ≪≫
                                        x.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (x.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                          { fst := y.fst ⋙ X_1.left, snd := y.snd ⋙ X_1.right,
                            iso :=
                              y.fst.associator X_1.left F₁ ≪≫
                                y.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (y.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight y.iso X_1.base ≪≫
                                      y.snd.associator G X_1.base ≪≫
                                        y.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (y.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X } },
                    map_id := ⋯, map_comp := ⋯ :
                    CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X ⥤
                      CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                  {
                    obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                      { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                        iso :=
                          S.fst.associator X_1.left F₁ ≪≫
                            S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                              (S.fst.associator F X_1.base).symm ≪≫
                                isoWhiskerRight S.iso X_1.base ≪≫
                                  S.snd.associator G X_1.base ≪≫
                                    S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                      (S.snd.associator X_1.right G₁).symm :
                        CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X },
                    map := fun {x y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X} (f : x ⟶ y) ↦
                      { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ :
                        Hom X
                          { fst := x.fst ⋙ X_1.left, snd := x.snd ⋙ X_1.right,
                            iso :=
                              x.fst.associator X_1.left F₁ ≪≫
                                x.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (x.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight x.iso X_1.base ≪≫
                                      x.snd.associator G X_1.base ≪≫
                                        x.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (x.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                          { fst := y.fst ⋙ X_1.left, snd := y.snd ⋙ X_1.right,
                            iso :=
                              y.fst.associator X_1.left F₁ ≪≫
                                y.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (y.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight y.iso X_1.base ≪≫
                                      y.snd.associator G X_1.base ≪≫
                                        y.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (y.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X } },
                    map_id := ⋯, map_comp := ⋯ :
                    CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X ⥤
                      CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X } }
              x).fst.app
        x_1 =
      NatTrans.app
        (Hom.fst
          (NatTrans.app
            (𝟙
              {
                obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                  { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                    iso :=
                      S.fst.associator X_1.left F₁ ≪≫
                        S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                          (S.fst.associator F X_1.base).symm ≪≫
                            isoWhiskerRight S.iso X_1.base ≪≫
                              S.snd.associator G X_1.base ≪≫
                                S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                  (S.snd.associator X_1.right G₁).symm },
                map := fun {x y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X} (f : x ⟶ y) ↦
                  { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ })
            x))
        x_1
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) (x_1 : X),
    (NatTrans.app
              {
                app := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                  {
                    fst :=
                      { app := fun (y : X) ↦ (CatCospanTransformMorphism.left (𝟙 X_1)).app (S.fst.obj y),
                        naturality := ⋯ :
                        NatTrans.{v₇, v₄, u₇, u₄} (C := X) (D := A₁)
                          (fst.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (B := B₁) (C := C₁) (F := F₁) (G := G₁)
                            ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                                { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                                  iso :=
                                    S.fst.associator X_1.left F₁ ≪≫
                                      S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                        (S.fst.associator F X_1.base).symm ≪≫
                                          isoWhiskerRight S.iso X_1.base ≪≫
                                            S.snd.associator G X_1.base ≪≫
                                              S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                                (S.snd.associator X_1.right G₁).symm :
                                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                              S))
                          (fst.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (B := B₁) (C := C₁) (F := F₁) (G := G₁)
                            ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                                { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                                  iso :=
                                    S.fst.associator X_1.left F₁ ≪≫
                                      S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                        (S.fst.associator F X_1.base).symm ≪≫
                                          isoWhiskerRight S.iso X_1.base ≪≫
                                            S.snd.associator G X_1.base ≪≫
                                              S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                                (S.snd.associator X_1.right G₁).symm :
                                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                              S)) },
                    snd :=
                      { app := fun (y : X) ↦ (CatCospanTransformMorphism.right (𝟙 X_1)).app (S.snd.obj y),
                        naturality := ⋯ :
                        NatTrans.{v₇, v₆, u₇, u₆} (C := X) (D := C₁)
                          (snd.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (A := A₁) (B := B₁) (F := F₁) (G := G₁)
                            ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                                { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                                  iso :=
                                    S.fst.associator X_1.left F₁ ≪≫
                                      S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                        (S.fst.associator F X_1.base).symm ≪≫
                                          isoWhiskerRight S.iso X_1.base ≪≫
                                            S.snd.associator G X_1.base ≪≫
                                              S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                                (S.snd.associator X_1.right G₁).symm :
                                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                              S))
                          (snd.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (A := A₁) (B := B₁) (F := F₁) (G := G₁)
                            ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                                { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                                  iso :=
                                    S.fst.associator X_1.left F₁ ≪≫
                                      S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                        (S.fst.associator F X_1.base).symm ≪≫
                                          isoWhiskerRight S.iso X_1.base ≪≫
                                            S.snd.associator G X_1.base ≪≫
                                              S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                                (S.snd.associator X_1.right G₁).symm :
                                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                              S)) },
                    w := ⋯ :
                    Hom.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (A := A₁) (B := B₁) (C := C₁) (F := F₁) (G := G₁) X
                      ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                          { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                            iso :=
                              S.fst.associator X_1.left F₁ ≪≫
                                S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (S.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight S.iso X_1.base ≪≫
                                      S.snd.associator G X_1.base ≪≫
                                        S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (S.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                        S)
                      ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                          { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                            iso :=
                              S.fst.associator X_1.left F₁ ≪≫
                                S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (S.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight S.iso X_1.base ≪≫
                                      S.snd.associator G X_1.base ≪≫
                                        S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (S.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X })
                        S) },
                naturality := ⋯ :
                NatTrans (C := CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) (D :=
                  CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X)
                  {
                    obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                      { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                        iso :=
                          S.fst.associator X_1.left F₁ ≪≫
                            S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                              (S.fst.associator F X_1.base).symm ≪≫
                                isoWhiskerRight S.iso X_1.base ≪≫
                                  S.snd.associator G X_1.base ≪≫
                                    S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                      (S.snd.associator X_1.right G₁).symm :
                        CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X },
                    map := fun {x y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X} (f : x ⟶ y) ↦
                      { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ :
                        Hom X
                          { fst := x.fst ⋙ X_1.left, snd := x.snd ⋙ X_1.right,
                            iso :=
                              x.fst.associator X_1.left F₁ ≪≫
                                x.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (x.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight x.iso X_1.base ≪≫
                                      x.snd.associator G X_1.base ≪≫
                                        x.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (x.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                          { fst := y.fst ⋙ X_1.left, snd := y.snd ⋙ X_1.right,
                            iso :=
                              y.fst.associator X_1.left F₁ ≪≫
                                y.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (y.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight y.iso X_1.base ≪≫
                                      y.snd.associator G X_1.base ≪≫
                                        y.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (y.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X } },
                    map_id := ⋯, map_comp := ⋯ :
                    CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X ⥤
                      CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                  {
                    obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                      { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                        iso :=
                          S.fst.associator X_1.left F₁ ≪≫
                            S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                              (S.fst.associator F X_1.base).symm ≪≫
                                isoWhiskerRight S.iso X_1.base ≪≫
                                  S.snd.associator G X_1.base ≪≫
                                    S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                      (S.snd.associator X_1.right G₁).symm :
                        CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X },
                    map := fun {x y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X} (f : x ⟶ y) ↦
                      { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ :
                        Hom X
                          { fst := x.fst ⋙ X_1.left, snd := x.snd ⋙ X_1.right,
                            iso :=
                              x.fst.associator X_1.left F₁ ≪≫
                                x.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (x.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight x.iso X_1.base ≪≫
                                      x.snd.associator G X_1.base ≪≫
                                        x.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (x.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                          { fst := y.fst ⋙ X_1.left, snd := y.snd ⋙ X_1.right,
                            iso :=
                              y.fst.associator X_1.left F₁ ≪≫
                                y.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                                  (y.fst.associator F X_1.base).symm ≪≫
                                    isoWhiskerRight y.iso X_1.base ≪≫
                                      y.snd.associator G X_1.base ≪≫
                                        y.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                          (y.snd.associator X_1.right G₁).symm :
                            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X } },
                    map_id := ⋯, map_comp := ⋯ :
                    CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X ⥤
                      CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X } }
              x).snd.app
        x_1 =
      NatTrans.app
        (Hom.snd
          (NatTrans.app
            (𝟙
              {
                obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                  { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
                    iso :=
                      S.fst.associator X_1.left F₁ ≪≫
                        S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                          (S.fst.associator F X_1.base).symm ≪≫
                            isoWhiskerRight S.iso X_1.base ≪≫
                              S.snd.associator G X_1.base ≪≫
                                S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                                  (S.snd.associator X_1.right G₁).symm },
                map := fun {x y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X} (f : x ⟶ y) ↦
                  { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ })
            x))
        x_1
⊢ Eq (α :=
    Quiver.Hom (V :=
      CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X ⥤ CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X)
      {
        obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
          { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
            iso :=
              S.fst.associator X_1.left F₁ ≪≫
                S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                  (S.fst.associator F X_1.base).symm ≪≫
                    isoWhiskerRight S.iso X_1.base ≪≫
                      S.snd.associator G X_1.base ≪≫
                        S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                          (S.snd.associator X_1.right G₁).symm },
        map := fun {x y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X} (f : x ⟶ y) ↦
          { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ },
        map_id := ⋯, map_comp := ⋯ }
      {
        obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
          { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
            iso :=
              S.fst.associator X_1.left F₁ ≪≫
                S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                  (S.fst.associator F X_1.base).symm ≪≫
                    isoWhiskerRight S.iso X_1.base ≪≫
                      S.snd.associator G X_1.base ≪≫
                        S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                          (S.snd.associator X_1.right G₁).symm },
        map := fun {x y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X} (f : x ⟶ y) ↦
          { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ },
        map_id := ⋯, map_comp := ⋯ })
    {
      app := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
        { fst := { app := fun (y : X) ↦ (CatCospanTransformMorphism.left (𝟙 X_1)).app (S.fst.obj y), naturality := ⋯ },
          snd := { app := fun (y : X) ↦ (CatCospanTransformMorphism.right (𝟙 X_1)).app (S.snd.obj y), naturality := ⋯ },
          w := ⋯ },
      naturality := ⋯ }
    (𝟙
      {
        obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
          { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
            iso :=
              S.fst.associator X_1.left F₁ ≪≫
                S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                  (S.fst.associator F X_1.base).symm ≪≫
                    isoWhiskerRight S.iso X_1.base ≪≫
                      S.snd.associator G X_1.base ≪≫
                        S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                          (S.snd.associator X_1.right G₁).symm },
        map := fun {x y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X} (f : x ⟶ y) ↦
          { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ },
        map_id := ⋯, map_comp := ⋯ })

Tactic:
ext