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