-- 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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
inst_5 : Category.{v₆, u₆} Z
X_1 Y_1 Z_1 : Functor.{v₄, v₅, u₄, u₅} X Y
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z_1
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (x_1 : X),
    ({
                  app := fun (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                    { fst := whiskerRight (f ≫ g) x.fst, snd := whiskerRight (f ≫ g) x.snd, 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 Y) ↦
                            { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                              iso :=
                                X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
                          x)
                        ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                            { fst := Z_1 ⋙ S.fst, snd := Z_1 ⋙ S.snd,
                              iso :=
                                Z_1.associator S.fst F ≪≫ Z_1.isoWhiskerLeft S.iso ≪≫ (Z_1.associator S.snd G).symm :
                              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
                          x) },
                  naturality := ⋯ :
                  NatTrans (C := CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (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 Y) ↦
                        { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                          iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                          CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
                      map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
                        { fst := X_1.whiskerLeft φ.fst, snd := X_1.whiskerLeft φ.snd, w := ⋯ :
                          Hom X
                            { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                              iso :=
                                X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                            { fst := X_1 ⋙ S'.fst, snd := X_1 ⋙ S'.snd,
                              iso :=
                                X_1.associator S'.fst F ≪≫ X_1.isoWhiskerLeft S'.iso ≪≫ (X_1.associator S'.snd 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 Y ⥤
                        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 Y) ↦
                        { fst := Z_1 ⋙ S.fst, snd := Z_1 ⋙ S.snd,
                          iso := Z_1.associator S.fst F ≪≫ Z_1.isoWhiskerLeft S.iso ≪≫ (Z_1.associator S.snd G).symm :
                          CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
                      map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
                        { fst := Z_1.whiskerLeft φ.fst, snd := Z_1.whiskerLeft φ.snd, w := ⋯ :
                          Hom X
                            { fst := Z_1 ⋙ S.fst, snd := Z_1 ⋙ S.snd,
                              iso :=
                                Z_1.associator S.fst F ≪≫ Z_1.isoWhiskerLeft S.iso ≪≫ (Z_1.associator S.snd G).symm :
                              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                            { fst := Z_1 ⋙ S'.fst, snd := Z_1 ⋙ S'.snd,
                              iso :=
                                Z_1.associator S'.fst F ≪≫ Z_1.isoWhiskerLeft S'.iso ≪≫ (Z_1.associator S'.snd 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 Y ⥤
                        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X } }.app
              x).fst.app
        x_1 =
      NatTrans.app
        (Hom.fst
          (NatTrans.app
            ({
                app := fun (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                  { fst := whiskerRight f x.fst, snd := whiskerRight f x.snd, 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 Y) ↦
                          { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                            iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                            CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
                        x)
                      ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                          { fst := Y_1 ⋙ S.fst, snd := Y_1 ⋙ S.snd,
                            iso := Y_1.associator S.fst F ≪≫ Y_1.isoWhiskerLeft S.iso ≪≫ (Y_1.associator S.snd G).symm :
                            CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
                        x) },
                naturality := ⋯ :
                NatTrans (C := CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (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 Y) ↦
                      { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                        iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
                    map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
                      { fst := X_1.whiskerLeft φ.fst, snd := X_1.whiskerLeft φ.snd, w := ⋯ :
                        Hom X
                          { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                            iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                            CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                          { fst := X_1 ⋙ S'.fst, snd := X_1 ⋙ S'.snd,
                            iso :=
                              X_1.associator S'.fst F ≪≫ X_1.isoWhiskerLeft S'.iso ≪≫ (X_1.associator S'.snd 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 Y ⥤
                      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 Y) ↦
                      { fst := Y_1 ⋙ S.fst, snd := Y_1 ⋙ S.snd,
                        iso := Y_1.associator S.fst F ≪≫ Y_1.isoWhiskerLeft S.iso ≪≫ (Y_1.associator S.snd G).symm :
                        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
                    map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
                      { fst := Y_1.whiskerLeft φ.fst, snd := Y_1.whiskerLeft φ.snd, w := ⋯ :
                        Hom X
                          { fst := Y_1 ⋙ S.fst, snd := Y_1 ⋙ S.snd,
                            iso := Y_1.associator S.fst F ≪≫ Y_1.isoWhiskerLeft S.iso ≪≫ (Y_1.associator S.snd G).symm :
                            CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                          { fst := Y_1 ⋙ S'.fst, snd := Y_1 ⋙ S'.snd,
                            iso :=
                              Y_1.associator S'.fst F ≪≫ Y_1.isoWhiskerLeft S'.iso ≪≫ (Y_1.associator S'.snd 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 Y ⥤
                      CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X } } ≫
              {
                app := fun (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                  { fst := whiskerRight g x.fst, snd := whiskerRight g x.snd, w := ⋯ },
                naturality := ⋯ })
            x))
        x_1
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (x_1 : X),
    ({
                  app := fun (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                    { fst := whiskerRight (f ≫ g) x.fst, snd := whiskerRight (f ≫ g) x.snd, 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 Y) ↦
                            { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                              iso :=
                                X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
                          x)
                        ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                            { fst := Z_1 ⋙ S.fst, snd := Z_1 ⋙ S.snd,
                              iso :=
                                Z_1.associator S.fst F ≪≫ Z_1.isoWhiskerLeft S.iso ≪≫ (Z_1.associator S.snd G).symm :
                              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
                          x) },
                  naturality := ⋯ :
                  NatTrans (C := CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (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 Y) ↦
                        { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                          iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                          CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
                      map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
                        { fst := X_1.whiskerLeft φ.fst, snd := X_1.whiskerLeft φ.snd, w := ⋯ :
                          Hom X
                            { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                              iso :=
                                X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                            { fst := X_1 ⋙ S'.fst, snd := X_1 ⋙ S'.snd,
                              iso :=
                                X_1.associator S'.fst F ≪≫ X_1.isoWhiskerLeft S'.iso ≪≫ (X_1.associator S'.snd 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 Y ⥤
                        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 Y) ↦
                        { fst := Z_1 ⋙ S.fst, snd := Z_1 ⋙ S.snd,
                          iso := Z_1.associator S.fst F ≪≫ Z_1.isoWhiskerLeft S.iso ≪≫ (Z_1.associator S.snd G).symm :
                          CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
                      map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
                        { fst := Z_1.whiskerLeft φ.fst, snd := Z_1.whiskerLeft φ.snd, w := ⋯ :
                          Hom X
                            { fst := Z_1 ⋙ S.fst, snd := Z_1 ⋙ S.snd,
                              iso :=
                                Z_1.associator S.fst F ≪≫ Z_1.isoWhiskerLeft S.iso ≪≫ (Z_1.associator S.snd G).symm :
                              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                            { fst := Z_1 ⋙ S'.fst, snd := Z_1 ⋙ S'.snd,
                              iso :=
                                Z_1.associator S'.fst F ≪≫ Z_1.isoWhiskerLeft S'.iso ≪≫ (Z_1.associator S'.snd 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 Y ⥤
                        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X } }.app
              x).snd.app
        x_1 =
      NatTrans.app
        (Hom.snd
          (NatTrans.app
            ({
                app := fun (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                  { fst := whiskerRight f x.fst, snd := whiskerRight f x.snd, 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 Y) ↦
                          { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                            iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                            CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
                        x)
                      ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                          { fst := Y_1 ⋙ S.fst, snd := Y_1 ⋙ S.snd,
                            iso := Y_1.associator S.fst F ≪≫ Y_1.isoWhiskerLeft S.iso ≪≫ (Y_1.associator S.snd G).symm :
                            CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
                        x) },
                naturality := ⋯ :
                NatTrans (C := CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (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 Y) ↦
                      { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                        iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
                    map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
                      { fst := X_1.whiskerLeft φ.fst, snd := X_1.whiskerLeft φ.snd, w := ⋯ :
                        Hom X
                          { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                            iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                            CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                          { fst := X_1 ⋙ S'.fst, snd := X_1 ⋙ S'.snd,
                            iso :=
                              X_1.associator S'.fst F ≪≫ X_1.isoWhiskerLeft S'.iso ≪≫ (X_1.associator S'.snd 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 Y ⥤
                      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 Y) ↦
                      { fst := Y_1 ⋙ S.fst, snd := Y_1 ⋙ S.snd,
                        iso := Y_1.associator S.fst F ≪≫ Y_1.isoWhiskerLeft S.iso ≪≫ (Y_1.associator S.snd G).symm :
                        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
                    map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
                      { fst := Y_1.whiskerLeft φ.fst, snd := Y_1.whiskerLeft φ.snd, w := ⋯ :
                        Hom X
                          { fst := Y_1 ⋙ S.fst, snd := Y_1 ⋙ S.snd,
                            iso := Y_1.associator S.fst F ≪≫ Y_1.isoWhiskerLeft S.iso ≪≫ (Y_1.associator S.snd G).symm :
                            CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                          { fst := Y_1 ⋙ S'.fst, snd := Y_1 ⋙ S'.snd,
                            iso :=
                              Y_1.associator S'.fst F ≪≫ Y_1.isoWhiskerLeft S'.iso ≪≫ (Y_1.associator S'.snd 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 Y ⥤
                      CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X } } ≫
              {
                app := fun (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                  { fst := whiskerRight g x.fst, snd := whiskerRight g x.snd, w := ⋯ },
                naturality := ⋯ })
            x))
        x_1
⊢ {
      app := fun (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
        { fst := whiskerRight (f ≫ g) x.fst, snd := whiskerRight (f ≫ g) x.snd, 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 Y) ↦
                { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                  iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                  CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
              x)
            ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                { fst := Z_1 ⋙ S.fst, snd := Z_1 ⋙ S.snd,
                  iso := Z_1.associator S.fst F ≪≫ Z_1.isoWhiskerLeft S.iso ≪≫ (Z_1.associator S.snd G).symm :
                  CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
              x) },
      naturality := ⋯ :
      NatTrans (C := CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (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 Y) ↦
            { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
              iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
          map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
            { fst := X_1.whiskerLeft φ.fst, snd := X_1.whiskerLeft φ.snd, w := ⋯ :
              Hom X
                { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                  iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                  CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                { fst := X_1 ⋙ S'.fst, snd := X_1 ⋙ S'.snd,
                  iso := X_1.associator S'.fst F ≪≫ X_1.isoWhiskerLeft S'.iso ≪≫ (X_1.associator S'.snd 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 Y ⥤ 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 Y) ↦
            { fst := Z_1 ⋙ S.fst, snd := Z_1 ⋙ S.snd,
              iso := Z_1.associator S.fst F ≪≫ Z_1.isoWhiskerLeft S.iso ≪≫ (Z_1.associator S.snd G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
          map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
            { fst := Z_1.whiskerLeft φ.fst, snd := Z_1.whiskerLeft φ.snd, w := ⋯ :
              Hom X
                { fst := Z_1 ⋙ S.fst, snd := Z_1 ⋙ S.snd,
                  iso := Z_1.associator S.fst F ≪≫ Z_1.isoWhiskerLeft S.iso ≪≫ (Z_1.associator S.snd G).symm :
                  CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                { fst := Z_1 ⋙ S'.fst, snd := Z_1 ⋙ S'.snd,
                  iso := Z_1.associator S'.fst F ≪≫ Z_1.isoWhiskerLeft S'.iso ≪≫ (Z_1.associator S'.snd 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 Y ⥤
            CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X } } =
    {
        app := fun (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
          { fst := whiskerRight f x.fst, snd := whiskerRight f x.snd, 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 Y) ↦
                  { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                    iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                    CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
                x)
              ((fun (S : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
                  { fst := Y_1 ⋙ S.fst, snd := Y_1 ⋙ S.snd,
                    iso := Y_1.associator S.fst F ≪≫ Y_1.isoWhiskerLeft S.iso ≪≫ (Y_1.associator S.snd G).symm :
                    CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })
                x) },
        naturality := ⋯ :
        NatTrans (C := CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (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 Y) ↦
              { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
            map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
              { fst := X_1.whiskerLeft φ.fst, snd := X_1.whiskerLeft φ.snd, w := ⋯ :
                Hom X
                  { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
                    iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm :
                    CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                  { fst := X_1 ⋙ S'.fst, snd := X_1 ⋙ S'.snd,
                    iso := X_1.associator S'.fst F ≪≫ X_1.isoWhiskerLeft S'.iso ≪≫ (X_1.associator S'.snd 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 Y ⥤
              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 Y) ↦
              { fst := Y_1 ⋙ S.fst, snd := Y_1 ⋙ S.snd,
                iso := Y_1.associator S.fst F ≪≫ Y_1.isoWhiskerLeft S.iso ≪≫ (Y_1.associator S.snd G).symm :
                CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X },
            map := fun {S S' : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y} (φ : S ⟶ S') ↦
              { fst := Y_1.whiskerLeft φ.fst, snd := Y_1.whiskerLeft φ.snd, w := ⋯ :
                Hom X
                  { fst := Y_1 ⋙ S.fst, snd := Y_1 ⋙ S.snd,
                    iso := Y_1.associator S.fst F ≪≫ Y_1.isoWhiskerLeft S.iso ≪≫ (Y_1.associator S.snd G).symm :
                    CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
                  { fst := Y_1 ⋙ S'.fst, snd := Y_1 ⋙ S'.snd,
                    iso := Y_1.associator S'.fst F ≪≫ Y_1.isoWhiskerLeft S'.iso ≪≫ (Y_1.associator S'.snd 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 Y ⥤
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X } } ≫
      {
        app := fun (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) ↦
          { fst := whiskerRight g x.fst, snd := whiskerRight g x.snd, w := ⋯ },
        naturality := ⋯ }

Tactic:
ext