Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: case h₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : X ⥤ F ⊡ G
x✝ : X
⊢ ((toCatCommSqOver F G X).map
              ((NatIso.ofComponents
                      (fun x ↦
                        NatIso.ofComponents
                          (fun x_1 ↦
                            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).fst)
                              (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).snd) ⋯)
                          ⋯)
                      ⋯).hom.app
                X✝) ≫
            (NatIso.ofComponents
                    (fun x ↦
                      CatCommSqOver.mkIso
                        (NatIso.ofComponents
                          (fun x_1 ↦
                            Iso.refl
                              (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj
                                      x).fst.obj
                                x_1))
                          ⋯)
                        (NatIso.ofComponents
                          (fun x_1 ↦
                            Iso.refl
                              (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj
                                      x).snd.obj
                                x_1))
                          ⋯)
                        ⋯)
                    ⋯).hom.app
              ((toCatCommSqOver F G X).obj X✝)).fst.app
      x✝ =
    (𝟙 ((toCatCommSqOver F G X).obj X✝)).fst.app x✝

pp: case h₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : X ⥤ F ⊡ G
x✝ : X
⊢ ((toCatCommSqOver F G X).map
              ((NatIso.ofComponents
                      (fun x ↦
                        NatIso.ofComponents
                          (fun x_1 ↦
                            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).fst)
                              (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).snd) ⋯)
                          ⋯)
                      ⋯).hom.app
                X✝) ≫
            (NatIso.ofComponents
                    (fun x ↦
                      CatCommSqOver.mkIso
                        (NatIso.ofComponents
                          (fun x_1 ↦
                            Iso.refl
                              (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj
                                      x).fst.obj
                                x_1))
                          ⋯)
                        (NatIso.ofComponents
                          (fun x_1 ↦
                            Iso.refl
                              (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj
                                      x).snd.obj
                                x_1))
                          ⋯)
                        ⋯)
                    ⋯).hom.app
              ((toCatCommSqOver F G X).obj X✝)).snd.app
      x✝ =
    (𝟙 ((toCatCommSqOver F G X).obj X✝)).snd.app x✝

Tactic:
<;>

Goal state after:
case h₁
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : X ⥤ F ⊡ G
x✝ : X
⊢ ((toCatCommSqOver F G X).map
              ((NatIso.ofComponents
                      (fun x ↦
                        NatIso.ofComponents
                          (fun x_1 ↦
                            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).fst)
                              (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).snd) ⋯)
                          ⋯)
                      ⋯).hom.app
                X✝) ≫
            (NatIso.ofComponents
                    (fun x ↦
                      CatCommSqOver.mkIso
                        (NatIso.ofComponents
                          (fun x_1 ↦
                            Iso.refl
                              (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj
                                      x).fst.obj
                                x_1))
                          ⋯)
                        (NatIso.ofComponents
                          (fun x_1 ↦
                            Iso.refl
                              (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj
                                      x).snd.obj
                                x_1))
                          ⋯)
                        ⋯)
                    ⋯).hom.app
              ((toCatCommSqOver F G X).obj X✝)).fst.app
      x✝ =
    (𝟙 ((toCatCommSqOver F G X).obj X✝)).fst.app x✝

case h₂
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
X✝ : X ⥤ F ⊡ G
x✝ : X
⊢ ((toCatCommSqOver F G X).map
              ((NatIso.ofComponents
                      (fun x ↦
                        NatIso.ofComponents
                          (fun x_1 ↦
                            mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).fst)
                              (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).snd) ⋯)
                          ⋯)
                      ⋯).hom.app
                X✝) ≫
            (NatIso.ofComponents
                    (fun x ↦
                      CatCommSqOver.mkIso
                        (NatIso.ofComponents
                          (fun x_1 ↦
                            Iso.refl
                              (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj
                                      x).fst.obj
                                x_1))
                          ⋯)
                        (NatIso.ofComponents
                          (fun x_1 ↦
                            Iso.refl
                              (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj
                                      x).snd.obj
                                x_1))
                          ⋯)
                        ⋯)
                    ⋯).hom.app
              ((toCatCommSqOver F G X).obj X✝)).snd.app
      x✝ =
    (𝟙 ((toCatCommSqOver F G X).obj X✝)).snd.app x✝