-- 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 : X ⥤ F ⊡ G
f : X_1 ⟶ Y
w :
  ∀ (x : X),
    Eq (α :=
      ((obj (𝟭 (X ⥤ F ⊡ G)) X_1).obj x).fst ⟶
        ((obj (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) Y).obj x).fst)
      (Hom.fst
        (NatTrans.app
          (map (𝟭 (X ⥤ F ⊡ G)) f ≫
            Iso.hom
              ((fun (x : X ⥤ F ⊡ G) ↦
                  NatIso.ofComponents
                    (fun (x_1 : X) ↦
                      mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                        (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) ⋯)
                    ⋯)
                Y))
          x))
      (Hom.fst
        (NatTrans.app
          (Iso.hom
              ((fun (x : X ⥤ F ⊡ G) ↦
                  NatIso.ofComponents
                    (fun (x_1 : X) ↦
                      mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                        (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) ⋯)
                    ⋯)
                X_1) ≫
            map (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) f)
          x))
⊢ Eq (α := obj (𝟭 (X ⥤ F ⊡ G)) X_1 ⟶ obj (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) Y)
    (map (𝟭 (X ⥤ F ⊡ G)) f ≫
      Iso.hom
        ((fun (x : X ⥤ F ⊡ G) ↦
            NatIso.ofComponents
              (fun (x_1 : X) ↦
                mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst) (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd)
                  ⋯)
              ⋯)
          Y))
    (Iso.hom
        ((fun (x : X ⥤ F ⊡ G) ↦
            NatIso.ofComponents
              (fun (x_1 : X) ↦
                mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst) (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd)
                  ⋯)
              ⋯)
          X_1) ≫
      map (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) f)
have w₁ : ∀ (x : X),
  Eq (α :=
    ((obj (𝟭 (X ⥤ F ⊡ G)) X_1).obj x).snd ⟶
      ((obj (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) Y).obj x).snd)
    (Hom.snd
      (NatTrans.app
        (map (𝟭 (X ⥤ F ⊡ G)) f ≫
          Iso.hom
            ((fun (x : X ⥤ F ⊡ G) ↦
                NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                      (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) sorry)
                  sorry)
              Y))
        x))
    (Hom.snd
      (NatTrans.app
        (Iso.hom
            ((fun (x : X ⥤ F ⊡ G) ↦
                NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                      (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) sorry)
                  sorry)
              X_1) ≫
          map (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) f)
        x))
Tactic: ext