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
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✝ Y✝ Z✝ : CatCospanTransform F G F₁ G₁
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ ({
                app := fun S ↦
                  { fst := { app := fun y ↦ (f✝ ≫ g✝).left.app (S.fst.obj y), naturality := ⋯ },
                    snd := { app := fun y ↦ (f✝ ≫ g✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).fst.app
      x✝ =
    (({
                  app := fun S ↦
                    { fst := { app := fun y ↦ f✝.left.app (S.fst.obj y), naturality := ⋯ },
                      snd := { app := fun y ↦ f✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                  naturality := ⋯ } ≫
                {
                  app := fun S ↦
                    { fst := { app := fun y ↦ g✝.left.app (S.fst.obj y), naturality := ⋯ },
                      snd := { app := fun y ↦ g✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                  naturality := ⋯ }).app
            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
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✝ Y✝ Z✝ : CatCospanTransform F G F₁ G₁
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ ({
                app := fun S ↦
                  { fst := { app := fun y ↦ (f✝ ≫ g✝).left.app (S.fst.obj y), naturality := ⋯ },
                    snd := { app := fun y ↦ (f✝ ≫ g✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).snd.app
      x✝ =
    (({
                  app := fun S ↦
                    { fst := { app := fun y ↦ f✝.left.app (S.fst.obj y), naturality := ⋯ },
                      snd := { app := fun y ↦ f✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                  naturality := ⋯ } ≫
                {
                  app := fun S ↦
                    { fst := { app := fun y ↦ g✝.left.app (S.fst.obj y), naturality := ⋯ },
                      snd := { app := fun y ↦ g✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                  naturality := ⋯ }).app
            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
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✝ Y✝ Z✝ : CatCospanTransform F G F₁ G₁
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ ({
                app := fun S ↦
                  { fst := { app := fun y ↦ (f✝ ≫ g✝).left.app (S.fst.obj y), naturality := ⋯ },
                    snd := { app := fun y ↦ (f✝ ≫ g✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).fst.app
      x✝ =
    (({
                  app := fun S ↦
                    { fst := { app := fun y ↦ f✝.left.app (S.fst.obj y), naturality := ⋯ },
                      snd := { app := fun y ↦ f✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                  naturality := ⋯ } ≫
                {
                  app := fun S ↦
                    { fst := { app := fun y ↦ g✝.left.app (S.fst.obj y), naturality := ⋯ },
                      snd := { app := fun y ↦ g✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                  naturality := ⋯ }).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✝ Y✝ Z✝ : CatCospanTransform F G F₁ G₁
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ ({
                app := fun S ↦
                  { fst := { app := fun y ↦ (f✝ ≫ g✝).left.app (S.fst.obj y), naturality := ⋯ },
                    snd := { app := fun y ↦ (f✝ ≫ g✝).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).snd.app
      x✝ =
    (({
                  app := fun S ↦
                    { fst := { app := fun y ↦ f✝.left.app (S.fst.obj y), naturality := ⋯ },
                      snd := { app := fun y ↦ f✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                  naturality := ⋯ } ≫
                {
                  app := fun S ↦
                    { fst := { app := fun y ↦ g✝.left.app (S.fst.obj y), naturality := ⋯ },
                      snd := { app := fun y ↦ g✝.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
                  naturality := ⋯ }).app
            x✝¹).snd.app
      x✝