-- 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
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
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).snd =
    CategoricalPullback.Hom.snd
      (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)

Tactic:
simp