-- 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
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
w :
  ∀ (t : X),
    Eq (α :=
      obj.{v₇, v₅, u₇, u₅}
          (fst.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (B := B₁) (C := C₁) (F := F₁) (G := G₁)
              (obj
                {
                  obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                    { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                      iso :=
                        S.fst.associator ψ.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                            (S.fst.associator F ψ.base).symm ≪≫
                              isoWhiskerRight S.iso ψ.base ≪≫
                                S.snd.associator G ψ.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                    (S.snd.associator ψ.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 ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ :
                      Hom X
                        { fst := x.fst ⋙ ψ.left, snd := x.snd ⋙ ψ.right,
                          iso :=
                            x.fst.associator ψ.left F₁ ≪≫
                              x.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                                (x.fst.associator F ψ.base).symm ≪≫
                                  isoWhiskerRight x.iso ψ.base ≪≫
                                    x.snd.associator G ψ.base ≪≫
                                      x.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                        (x.snd.associator ψ.right G₁).symm :
                          CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                        { fst := y.fst ⋙ ψ.left, snd := y.snd ⋙ ψ.right,
                          iso :=
                            y.fst.associator ψ.left F₁ ≪≫
                              y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                                (y.fst.associator F ψ.base).symm ≪≫
                                  isoWhiskerRight y.iso ψ.base ≪≫
                                    y.snd.associator G ψ.base ≪≫
                                      y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                        (y.snd.associator ψ.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 }
                S) ⋙
            F₁)
          t ⟶
        obj.{v₇, v₅, u₇, u₅}
          (snd.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (A := A₁) (B := B₁) (F := F₁) (G := G₁)
              (obj
                {
                  obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                    { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                      iso :=
                        S.fst.associator ψ'.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                            (S.fst.associator F ψ'.base).symm ≪≫
                              isoWhiskerRight S.iso ψ'.base ≪≫
                                S.snd.associator G ψ'.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                    (S.snd.associator ψ'.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 ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }
                S) ⋙
            G₁)
          t)
      (NatTrans.app
        (whiskerRight { app := fun (y : X) ↦ η.left.app (S.fst.obj y), naturality := ⋯ } F₁ ≫
          Iso.hom
            (iso
              (obj
                {
                  obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                    { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                      iso :=
                        S.fst.associator ψ'.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                            (S.fst.associator F ψ'.base).symm ≪≫
                              isoWhiskerRight S.iso ψ'.base ≪≫
                                S.snd.associator G ψ'.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                    (S.snd.associator ψ'.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 ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ :
                      Hom X
                        { fst := x.fst ⋙ ψ'.left, snd := x.snd ⋙ ψ'.right,
                          iso :=
                            x.fst.associator ψ'.left F₁ ≪≫
                              x.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                                (x.fst.associator F ψ'.base).symm ≪≫
                                  isoWhiskerRight x.iso ψ'.base ≪≫
                                    x.snd.associator G ψ'.base ≪≫
                                      x.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                        (x.snd.associator ψ'.right G₁).symm :
                          CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                        { fst := y.fst ⋙ ψ'.left, snd := y.snd ⋙ ψ'.right,
                          iso :=
                            y.fst.associator ψ'.left F₁ ≪≫
                              y.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                                (y.fst.associator F ψ'.base).symm ≪≫
                                  isoWhiskerRight y.iso ψ'.base ≪≫
                                    y.snd.associator G ψ'.base ≪≫
                                      y.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                        (y.snd.associator ψ'.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 }
                S)))
        t)
      (NatTrans.app
        (Iso.hom
            (iso
              (obj
                {
                  obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                    { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                      iso :=
                        S.fst.associator ψ.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                            (S.fst.associator F ψ.base).symm ≪≫
                              isoWhiskerRight S.iso ψ.base ≪≫
                                S.snd.associator G ψ.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                    (S.snd.associator ψ.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 ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ :
                      Hom X
                        { fst := x.fst ⋙ ψ.left, snd := x.snd ⋙ ψ.right,
                          iso :=
                            x.fst.associator ψ.left F₁ ≪≫
                              x.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                                (x.fst.associator F ψ.base).symm ≪≫
                                  isoWhiskerRight x.iso ψ.base ≪≫
                                    x.snd.associator G ψ.base ≪≫
                                      x.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                        (x.snd.associator ψ.right G₁).symm :
                          CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                        { fst := y.fst ⋙ ψ.left, snd := y.snd ⋙ ψ.right,
                          iso :=
                            y.fst.associator ψ.left F₁ ≪≫
                              y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                                (y.fst.associator F ψ.base).symm ≪≫
                                  isoWhiskerRight y.iso ψ.base ≪≫
                                    y.snd.associator G ψ.base ≪≫
                                      y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                        (y.snd.associator ψ.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 }
                S)) ≫
          whiskerRight { app := fun (y : X) ↦ η.right.app (S.snd.obj y), naturality := ⋯ } G₁)
        t)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₇, v₅, u₇, u₅} X B₁)
      (fst.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (B := B₁) (C := C₁) (F := F₁) (G := G₁)
          (obj
            {
              obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                  iso :=
                    S.fst.associator ψ.left F₁ ≪≫
                      S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                        (S.fst.associator F ψ.base).symm ≪≫
                          isoWhiskerRight S.iso ψ.base ≪≫
                            S.snd.associator G ψ.base ≪≫
                              S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                (S.snd.associator ψ.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 ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ }
            S) ⋙
        F₁)
      (snd.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} (A := A₁) (B := B₁) (F := F₁) (G := G₁)
          (obj
            {
              obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                  iso :=
                    S.fst.associator ψ'.left F₁ ≪≫
                      S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                        (S.fst.associator F ψ'.base).symm ≪≫
                          isoWhiskerRight S.iso ψ'.base ≪≫
                            S.snd.associator G ψ'.base ≪≫
                              S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                (S.snd.associator ψ'.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 ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ }
            S) ⋙
        G₁))
    (whiskerRight { app := fun (y : X) ↦ η.left.app (S.fst.obj y), naturality := ⋯ } F₁ ≫
      Iso.hom
        (iso
          (obj
            {
              obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                  iso :=
                    S.fst.associator ψ'.left F₁ ≪≫
                      S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                        (S.fst.associator F ψ'.base).symm ≪≫
                          isoWhiskerRight S.iso ψ'.base ≪≫
                            S.snd.associator G ψ'.base ≪≫
                              S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                (S.snd.associator ψ'.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 ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ :
                  Hom X
                    { fst := x.fst ⋙ ψ'.left, snd := x.snd ⋙ ψ'.right,
                      iso :=
                        x.fst.associator ψ'.left F₁ ≪≫
                          x.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                            (x.fst.associator F ψ'.base).symm ≪≫
                              isoWhiskerRight x.iso ψ'.base ≪≫
                                x.snd.associator G ψ'.base ≪≫
                                  x.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                    (x.snd.associator ψ'.right G₁).symm :
                      CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                    { fst := y.fst ⋙ ψ'.left, snd := y.snd ⋙ ψ'.right,
                      iso :=
                        y.fst.associator ψ'.left F₁ ≪≫
                          y.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                            (y.fst.associator F ψ'.base).symm ≪≫
                              isoWhiskerRight y.iso ψ'.base ≪≫
                                y.snd.associator G ψ'.base ≪≫
                                  y.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                    (y.snd.associator ψ'.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 }
            S)))
    (Iso.hom
        (iso
          (obj
            {
              obj := fun (S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) ↦
                { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                  iso :=
                    S.fst.associator ψ.left F₁ ≪≫
                      S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                        (S.fst.associator F ψ.base).symm ≪≫
                          isoWhiskerRight S.iso ψ.base ≪≫
                            S.snd.associator G ψ.base ≪≫
                              S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                (S.snd.associator ψ.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 ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ :
                  Hom X
                    { fst := x.fst ⋙ ψ.left, snd := x.snd ⋙ ψ.right,
                      iso :=
                        x.fst.associator ψ.left F₁ ≪≫
                          x.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                            (x.fst.associator F ψ.base).symm ≪≫
                              isoWhiskerRight x.iso ψ.base ≪≫
                                x.snd.associator G ψ.base ≪≫
                                  x.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                    (x.snd.associator ψ.right G₁).symm :
                      CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }
                    { fst := y.fst ⋙ ψ.left, snd := y.snd ⋙ ψ.right,
                      iso :=
                        y.fst.associator ψ.left F₁ ≪≫
                          y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                            (y.fst.associator F ψ.base).symm ≪≫
                              isoWhiskerRight y.iso ψ.base ≪≫
                                y.snd.associator G ψ.base ≪≫
                                  y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                    (y.snd.associator ψ.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 }
            S)) ≫
      whiskerRight { app := fun (y : X) ↦ η.right.app (S.snd.obj y), naturality := ⋯ } G₁)

Tactic:
ext t