-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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₁
⊢ 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 := ⋯ })
have 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 := sorry :
                      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 := sorry :
                      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 := sorry :
                  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 := sorry :
              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 := sorry :
                      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 := sorry, map_comp := sorry :
                  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 := sorry :
                      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 := sorry, map_comp := sorry :
                  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 := sorry },
              map_id := sorry, map_comp := sorry })
          x))
      x_1
Tactic: ext