-- 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 : 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
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) ⋯)
                        ⋯)
                    ⋯))
                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.snd (𝟙 (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)

Tactic:
ext