-- 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 : X ⥤ F ⊡ G
h₁ :
  ∀ (x : X),
    NatTrans.app
        (CatCommSqOver.Hom.fst
          (map (toCatCommSqOver F G X)
              (NatTrans.app
                (Iso.hom
                  (NatIso.ofComponents
                    (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) ≫
            NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (fun (x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X) ↦
                    CatCommSqOver.mkIso
                      (NatIso.ofComponents
                        (fun (x_1 : X) ↦
                          Iso.refl
                            ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X)
                                    x).fst.obj
                              x_1))
                        ⋯)
                      (NatIso.ofComponents
                        (fun (x_1 : X) ↦
                          Iso.refl
                            ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X)
                                    x).snd.obj
                              x_1))
                        ⋯)
                      ⋯)
                  ⋯))
              (obj (toCatCommSqOver F G X) X_1)))
        x =
      (CatCommSqOver.Hom.fst (𝟙 (obj (toCatCommSqOver F G X) X_1))).app x
⊢ map (toCatCommSqOver F G X)
        (NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (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) ≫
      NatTrans.app
        (Iso.hom
          (NatIso.ofComponents
            (fun (x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X) ↦
              CatCommSqOver.mkIso
                (NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    Iso.refl
                      ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj
                        x_1))
                  ⋯)
                (NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    Iso.refl
                      ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj
                        x_1))
                  ⋯)
                ⋯)
            ⋯))
        (obj (toCatCommSqOver F G X) X_1) =
    𝟙 (obj (toCatCommSqOver F G X) X_1)
have h₂ : ∀ (x : X),
  NatTrans.app
      (CatCommSqOver.Hom.snd
        (map (toCatCommSqOver F G X)
            (NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (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)
                  sorry))
              X_1) ≫
          NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X) ↦
                  CatCommSqOver.mkIso
                    (NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        Iso.refl
                          ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj
                            x_1))
                      sorry)
                    (NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        Iso.refl
                          ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj
                            x_1))
                      sorry)
                    sorry)
                sorry))
            (obj (toCatCommSqOver F G X) X_1)))
      x =
    (CatCommSqOver.Hom.snd (𝟙 (obj (toCatCommSqOver F G X) X_1))).app x
Tactic: ext