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

Goal state before:
pp: 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
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✝ : CatCospanTransform F G F₁ G₁
⊢ {
      app := fun S ↦
        { fst := { app := fun y ↦ (𝟙 X✝).left.app (S.fst.obj y), naturality := ⋯ },
          snd := { app := fun y ↦ (𝟙 X✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
      naturality := ⋯ } =
    𝟙
      {
        obj := fun S ↦
          { fst := S.fst ⋙ X✝.left, snd := S.snd ⋙ X✝.right,
            iso :=
              S.fst.associator X✝.left F₁ ≪≫
                S.fst.isoWhiskerLeft (CatCommSq.iso F X✝.left X✝.base F₁).symm ≪≫
                  (S.fst.associator F X✝.base).symm ≪≫
                    isoWhiskerRight S.iso X✝.base ≪≫
                      S.snd.associator G X✝.base ≪≫
                        S.snd.isoWhiskerLeft (CatCommSq.iso G X✝.right X✝.base G₁) ≪≫
                          (S.snd.associator X✝.right G₁).symm },
        map := fun {x y} f ↦ { fst := whiskerRight f.fst X✝.left, snd := whiskerRight f.snd X✝.right, w := ⋯ },
        map_id := ⋯, map_comp := ⋯ }

Tactic:
ext

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
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✝ : CatCospanTransform F G F₁ G₁
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ ({
                app := fun S ↦
                  { fst := { app := fun y ↦ (𝟙 X✝).left.app (S.fst.obj y), naturality := ⋯ },
                    snd := { app := fun y ↦ (𝟙 X✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).fst.app
      x✝ =
    ((𝟙
                {
                  obj := fun S ↦
                    { fst := S.fst ⋙ X✝.left, snd := S.snd ⋙ X✝.right,
                      iso :=
                        S.fst.associator X✝.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F X✝.left X✝.base F₁).symm ≪≫
                            (S.fst.associator F X✝.base).symm ≪≫
                              isoWhiskerRight S.iso X✝.base ≪≫
                                S.snd.associator G X✝.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G X✝.right X✝.base G₁) ≪≫
                                    (S.snd.associator X✝.right G₁).symm },
                  map := fun {x y} f ↦
                    { fst := whiskerRight f.fst X✝.left, snd := whiskerRight f.snd X✝.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }).app
            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
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✝ : CatCospanTransform F G F₁ G₁
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ ({
                app := fun S ↦
                  { fst := { app := fun y ↦ (𝟙 X✝).left.app (S.fst.obj y), naturality := ⋯ },
                    snd := { app := fun y ↦ (𝟙 X✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).snd.app
      x✝ =
    ((𝟙
                {
                  obj := fun S ↦
                    { fst := S.fst ⋙ X✝.left, snd := S.snd ⋙ X✝.right,
                      iso :=
                        S.fst.associator X✝.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F X✝.left X✝.base F₁).symm ≪≫
                            (S.fst.associator F X✝.base).symm ≪≫
                              isoWhiskerRight S.iso X✝.base ≪≫
                                S.snd.associator G X✝.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G X✝.right X✝.base G₁) ≪≫
                                    (S.snd.associator X✝.right G₁).symm },
                  map := fun {x y} f ↦
                    { fst := whiskerRight f.fst X✝.left, snd := whiskerRight f.snd X✝.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }).app
            x✝¹).snd.app
      x✝