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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ ({ app := fun x ↦ { fst := whiskerRight (𝟙 X✝) x.fst, snd := whiskerRight (𝟙 X✝) x.snd, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).fst.app
      x✝ =
    ((𝟙
                {
                  obj := fun S ↦
                    { fst := X✝ ⋙ S.fst, snd := X✝ ⋙ S.snd,
                      iso := X✝.associator S.fst F ≪≫ X✝.isoWhiskerLeft S.iso ≪≫ (X✝.associator S.snd G).symm },
                  map := fun {S S'} φ ↦ { fst := X✝.whiskerLeft φ.fst, snd := X✝.whiskerLeft φ.snd, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }).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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ ({ app := fun x ↦ { fst := whiskerRight (𝟙 X✝) x.fst, snd := whiskerRight (𝟙 X✝) x.snd, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).snd.app
      x✝ =
    ((𝟙
                {
                  obj := fun S ↦
                    { fst := X✝ ⋙ S.fst, snd := X✝ ⋙ S.snd,
                      iso := X✝.associator S.fst F ≪≫ X✝.isoWhiskerLeft S.iso ≪≫ (X✝.associator S.snd G).symm },
                  map := fun {S S'} φ ↦ { fst := X✝.whiskerLeft φ.fst, snd := X✝.whiskerLeft φ.snd, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }).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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ ({ app := fun x ↦ { fst := whiskerRight (𝟙 X✝) x.fst, snd := whiskerRight (𝟙 X✝) x.snd, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).fst.app
      x✝ =
    ((𝟙
                {
                  obj := fun S ↦
                    { fst := X✝ ⋙ S.fst, snd := X✝ ⋙ S.snd,
                      iso := X✝.associator S.fst F ≪≫ X✝.isoWhiskerLeft S.iso ≪≫ (X✝.associator S.snd G).symm },
                  map := fun {S S'} φ ↦ { fst := X✝.whiskerLeft φ.fst, snd := X✝.whiskerLeft φ.snd, 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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
X✝ : X ⥤ Y
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ ({ app := fun x ↦ { fst := whiskerRight (𝟙 X✝) x.fst, snd := whiskerRight (𝟙 X✝) x.snd, w := ⋯ },
                naturality := ⋯ }.app
            x✝¹).snd.app
      x✝ =
    ((𝟙
                {
                  obj := fun S ↦
                    { fst := X✝ ⋙ S.fst, snd := X✝ ⋙ S.snd,
                      iso := X✝.associator S.fst F ≪≫ X✝.isoWhiskerLeft S.iso ≪≫ (X✝.associator S.snd G).symm },
                  map := fun {S S'} φ ↦ { fst := X✝.whiskerLeft φ.fst, snd := X✝.whiskerLeft φ.snd, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }).app
            x✝¹).snd.app
      x✝