-- 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 : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
f : X_1 ⟶ Y
g : Y ⟶ Z
w :
  ∀ (x : X),
    ({
              app := fun (x : X) ↦
                { fst := (f ≫ g).fst.app x, snd := (f ≫ g).snd.app x, w := ⋯ :
                  CategoricalPullback.Hom.{v₁, v₂, v₃, u₁, u₂, u₃} (A := A) (B := B) (C := C) (F := F) (G := G)
                    ((fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }) x)
                    ((fun (x : X) ↦ { fst := Z.fst.obj x, snd := Z.snd.obj x, iso := Z.iso.app x : F ⊡ G }) x) },
              naturality := ⋯ :
              NatTrans (C := X) (D := F ⊡ G)
                { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G },
                  map := fun {x y : X} (f : x ⟶ y) ↦
                    { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ :
                      { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }.Hom
                        { fst := X_1.fst.obj y, snd := X_1.snd.obj y, iso := X_1.iso.app y : F ⊡ G } },
                  map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G }
                { obj := fun (x : X) ↦ { fst := Z.fst.obj x, snd := Z.snd.obj x, iso := Z.iso.app x : F ⊡ G },
                  map := fun {x y : X} (f : x ⟶ y) ↦
                    { fst := Z.fst.map f, snd := Z.snd.map f, w := ⋯ :
                      { fst := Z.fst.obj x, snd := Z.snd.obj x, iso := Z.iso.app x : F ⊡ G }.Hom
                        { fst := Z.fst.obj y, snd := Z.snd.obj y, iso := Z.iso.app y : F ⊡ G } },
                  map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G } }.app
          x).fst =
      CategoricalPullback.Hom.fst
        (NatTrans.app
          ({
              app := fun (x : X) ↦
                { fst := f.fst.app x, snd := f.snd.app x, w := ⋯ :
                  CategoricalPullback.Hom.{v₁, v₂, v₃, u₁, u₂, u₃} (A := A) (B := B) (C := C) (F := F) (G := G)
                    ((fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }) x)
                    ((fun (x : X) ↦ { fst := Y.fst.obj x, snd := Y.snd.obj x, iso := Y.iso.app x : F ⊡ G }) x) },
              naturality := ⋯ :
              NatTrans (C := X) (D := F ⊡ G)
                { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G },
                  map := fun {x y : X} (f : x ⟶ y) ↦
                    { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ :
                      { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }.Hom
                        { fst := X_1.fst.obj y, snd := X_1.snd.obj y, iso := X_1.iso.app y : F ⊡ G } },
                  map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G }
                { obj := fun (x : X) ↦ { fst := Y.fst.obj x, snd := Y.snd.obj x, iso := Y.iso.app x : F ⊡ G },
                  map := fun {x y : X} (f : x ⟶ y) ↦
                    { fst := Y.fst.map f, snd := Y.snd.map f, w := ⋯ :
                      { fst := Y.fst.obj x, snd := Y.snd.obj x, iso := Y.iso.app x : F ⊡ G }.Hom
                        { fst := Y.fst.obj y, snd := Y.snd.obj y, iso := Y.iso.app y : F ⊡ G } },
                  map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G } } ≫
            { app := fun (x : X) ↦ { fst := g.fst.app x, snd := g.snd.app x, w := ⋯ }, naturality := ⋯ })
          x)
⊢ {
      app := fun (x : X) ↦
        { fst := (f ≫ g).fst.app x, snd := (f ≫ g).snd.app x, w := ⋯ :
          CategoricalPullback.Hom.{v₁, v₂, v₃, u₁, u₂, u₃} (A := A) (B := B) (C := C) (F := F) (G := G)
            ((fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }) x)
            ((fun (x : X) ↦ { fst := Z.fst.obj x, snd := Z.snd.obj x, iso := Z.iso.app x : F ⊡ G }) x) },
      naturality := ⋯ :
      NatTrans (C := X) (D := F ⊡ G)
        { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G },
          map := fun {x y : X} (f : x ⟶ y) ↦
            { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ :
              { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }.Hom
                { fst := X_1.fst.obj y, snd := X_1.snd.obj y, iso := X_1.iso.app y : F ⊡ G } },
          map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G }
        { obj := fun (x : X) ↦ { fst := Z.fst.obj x, snd := Z.snd.obj x, iso := Z.iso.app x : F ⊡ G },
          map := fun {x y : X} (f : x ⟶ y) ↦
            { fst := Z.fst.map f, snd := Z.snd.map f, w := ⋯ :
              { fst := Z.fst.obj x, snd := Z.snd.obj x, iso := Z.iso.app x : F ⊡ G }.Hom
                { fst := Z.fst.obj y, snd := Z.snd.obj y, iso := Z.iso.app y : F ⊡ G } },
          map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G } } =
    {
        app := fun (x : X) ↦
          { fst := f.fst.app x, snd := f.snd.app x, w := ⋯ :
            CategoricalPullback.Hom.{v₁, v₂, v₃, u₁, u₂, u₃} (A := A) (B := B) (C := C) (F := F) (G := G)
              ((fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }) x)
              ((fun (x : X) ↦ { fst := Y.fst.obj x, snd := Y.snd.obj x, iso := Y.iso.app x : F ⊡ G }) x) },
        naturality := ⋯ :
        NatTrans (C := X) (D := F ⊡ G)
          { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G },
            map := fun {x y : X} (f : x ⟶ y) ↦
              { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ :
                { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }.Hom
                  { fst := X_1.fst.obj y, snd := X_1.snd.obj y, iso := X_1.iso.app y : F ⊡ G } },
            map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G }
          { obj := fun (x : X) ↦ { fst := Y.fst.obj x, snd := Y.snd.obj x, iso := Y.iso.app x : F ⊡ G },
            map := fun {x y : X} (f : x ⟶ y) ↦
              { fst := Y.fst.map f, snd := Y.snd.map f, w := ⋯ :
                { fst := Y.fst.obj x, snd := Y.snd.obj x, iso := Y.iso.app x : F ⊡ G }.Hom
                  { fst := Y.fst.obj y, snd := Y.snd.obj y, iso := Y.iso.app y : F ⊡ G } },
            map_id := ⋯, map_comp := ⋯ : X ⥤ F ⊡ G } } ≫
      { app := fun (x : X) ↦ { fst := g.fst.app x, snd := g.snd.app x, w := ⋯ }, naturality := ⋯ }
have w₁ : ∀ (x : X),
  ({
            app := fun (x : X) ↦
              { fst := (f ≫ g).fst.app x, snd := (f ≫ g).snd.app x, w := sorry :
                CategoricalPullback.Hom.{v₁, v₂, v₃, u₁, u₂, u₃} (A := A) (B := B) (C := C) (F := F) (G := G)
                  ((fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }) x)
                  ((fun (x : X) ↦ { fst := Z.fst.obj x, snd := Z.snd.obj x, iso := Z.iso.app x : F ⊡ G }) x) },
            naturality := sorry :
            NatTrans (C := X) (D := F ⊡ G)
              { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G },
                map := fun {x y : X} (f : x ⟶ y) ↦
                  { fst := X_1.fst.map f, snd := X_1.snd.map f, w := sorry :
                    { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }.Hom
                      { fst := X_1.fst.obj y, snd := X_1.snd.obj y, iso := X_1.iso.app y : F ⊡ G } },
                map_id := sorry, map_comp := sorry : X ⥤ F ⊡ G }
              { obj := fun (x : X) ↦ { fst := Z.fst.obj x, snd := Z.snd.obj x, iso := Z.iso.app x : F ⊡ G },
                map := fun {x y : X} (f : x ⟶ y) ↦
                  { fst := Z.fst.map f, snd := Z.snd.map f, w := sorry :
                    { fst := Z.fst.obj x, snd := Z.snd.obj x, iso := Z.iso.app x : F ⊡ G }.Hom
                      { fst := Z.fst.obj y, snd := Z.snd.obj y, iso := Z.iso.app y : F ⊡ G } },
                map_id := sorry, map_comp := sorry : X ⥤ F ⊡ G } }.app
        x).snd =
    CategoricalPullback.Hom.snd
      (NatTrans.app
        ({
            app := fun (x : X) ↦
              { fst := f.fst.app x, snd := f.snd.app x, w := sorry :
                CategoricalPullback.Hom.{v₁, v₂, v₃, u₁, u₂, u₃} (A := A) (B := B) (C := C) (F := F) (G := G)
                  ((fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }) x)
                  ((fun (x : X) ↦ { fst := Y.fst.obj x, snd := Y.snd.obj x, iso := Y.iso.app x : F ⊡ G }) x) },
            naturality := sorry :
            NatTrans (C := X) (D := F ⊡ G)
              { obj := fun (x : X) ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G },
                map := fun {x y : X} (f : x ⟶ y) ↦
                  { fst := X_1.fst.map f, snd := X_1.snd.map f, w := sorry :
                    { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x : F ⊡ G }.Hom
                      { fst := X_1.fst.obj y, snd := X_1.snd.obj y, iso := X_1.iso.app y : F ⊡ G } },
                map_id := sorry, map_comp := sorry : X ⥤ F ⊡ G }
              { obj := fun (x : X) ↦ { fst := Y.fst.obj x, snd := Y.snd.obj x, iso := Y.iso.app x : F ⊡ G },
                map := fun {x y : X} (f : x ⟶ y) ↦
                  { fst := Y.fst.map f, snd := Y.snd.map f, w := sorry :
                    { fst := Y.fst.obj x, snd := Y.snd.obj x, iso := Y.iso.app x : F ⊡ G }.Hom
                      { fst := Y.fst.obj y, snd := Y.snd.obj y, iso := Y.iso.app y : F ⊡ G } },
                map_id := sorry, map_comp := sorry : X ⥤ F ⊡ G } } ≫
          { app := fun (x : X) ↦ { fst := g.fst.app x, snd := g.snd.app x, w := sorry }, naturality := sorry })
        x)
Tactic: ext