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