-- 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
ψ : CatCospanTransform F G F₁ G₁
X_1 Y Z : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
f : X_1 ⟶ Y
g : Y ⟶ Z
h₁ :
  ∀ (x : X),
    Eq.{v₄ + 1} (α :=
      { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
                iso :=
                  X_1.fst.associator ψ.left F₁ ≪≫
                    X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                      (X_1.fst.associator F ψ.base).symm ≪≫
                        isoWhiskerRight X_1.iso ψ.base ≪≫
                          X_1.snd.associator G ψ.base ≪≫
                            X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                              (X_1.snd.associator ψ.right G₁).symm :
                CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.fst.obj
          x ⟶
        { fst := Z.fst ⋙ ψ.left, snd := Z.snd ⋙ ψ.right,
                iso :=
                  Z.fst.associator ψ.left F₁ ≪≫
                    Z.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                      (Z.fst.associator F ψ.base).symm ≪≫
                        isoWhiskerRight Z.iso ψ.base ≪≫
                          Z.snd.associator G ψ.base ≪≫
                            Z.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                              (Z.snd.associator ψ.right G₁).symm :
                CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.fst.obj
          x)
      (NatTrans.app
        (Hom.fst { fst := whiskerRight (f ≫ g).fst ψ.left, snd := whiskerRight (f ≫ g).snd ψ.right, w := ⋯ }) x)
      (NatTrans.app
        (Hom.fst
          (CategoryStruct.comp (Y :=
            { 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 })
            { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ }
            { fst := whiskerRight g.fst ψ.left, snd := whiskerRight g.snd ψ.right, w := ⋯ }))
        x)
⊢ Eq (α :=
    { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
        iso :=
          X_1.fst.associator ψ.left F₁ ≪≫
            X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
              (X_1.fst.associator F ψ.base).symm ≪≫
                isoWhiskerRight X_1.iso ψ.base ≪≫
                  X_1.snd.associator G ψ.base ≪≫
                    X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫ (X_1.snd.associator ψ.right G₁).symm :
        CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X } ⟶
      { fst := Z.fst ⋙ ψ.left, snd := Z.snd ⋙ ψ.right,
        iso :=
          Z.fst.associator ψ.left F₁ ≪≫
            Z.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
              (Z.fst.associator F ψ.base).symm ≪≫
                isoWhiskerRight Z.iso ψ.base ≪≫
                  Z.snd.associator G ψ.base ≪≫
                    Z.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫ (Z.snd.associator ψ.right G₁).symm })
    { fst := whiskerRight (f ≫ g).fst ψ.left, snd := whiskerRight (f ≫ g).snd ψ.right, w := ⋯ }
    (CategoryStruct.comp (Y :=
      { 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 })
      { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ }
      { fst := whiskerRight g.fst ψ.left, snd := whiskerRight g.snd ψ.right, w := ⋯ })
have h₂ : ∀ (x : X),
  Eq.{v₆ + 1} (α :=
    { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
              iso :=
                X_1.fst.associator ψ.left F₁ ≪≫
                  X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (X_1.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight X_1.iso ψ.base ≪≫
                        X_1.snd.associator G ψ.base ≪≫
                          X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (X_1.snd.associator ψ.right G₁).symm :
              CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.snd.obj
        x ⟶
      { fst := Z.fst ⋙ ψ.left, snd := Z.snd ⋙ ψ.right,
              iso :=
                Z.fst.associator ψ.left F₁ ≪≫
                  Z.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (Z.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight Z.iso ψ.base ≪≫
                        Z.snd.associator G ψ.base ≪≫
                          Z.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (Z.snd.associator ψ.right G₁).symm :
              CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.snd.obj
        x)
    (NatTrans.app (Hom.snd { fst := whiskerRight (f ≫ g).fst ψ.left, snd := whiskerRight (f ≫ g).snd ψ.right, w := sorry })
      x)
    (NatTrans.app
      (Hom.snd
        (CategoryStruct.comp (Y :=
          { 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 })
          { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := sorry }
          { fst := whiskerRight g.fst ψ.left, snd := whiskerRight g.snd ψ.right, w := sorry }))
      x)
Tactic: ext