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
ψ : CatCospanTransform F G F₁ G₁
X✝ : CatCommSqOver F G X
⊢ { fst := whiskerRight (𝟙 X✝).fst ψ.left, snd := whiskerRight (𝟙 X✝).snd ψ.right, w := ⋯ } =
    𝟙
      { fst := X✝.fst ⋙ ψ.left, snd := X✝.snd ⋙ ψ.right,
        iso :=
          X✝.fst.associator ψ.left F₁ ≪≫
            X✝.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
              (X✝.fst.associator F ψ.base).symm ≪≫
                isoWhiskerRight X✝.iso ψ.base ≪≫
                  X✝.snd.associator G ψ.base ≪≫
                    X✝.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫ (X✝.snd.associator ψ.right G₁).symm }

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
ψ : CatCospanTransform F G F₁ G₁
X✝ : CatCommSqOver F G X
x✝ : X
⊢ { fst := whiskerRight (𝟙 X✝).fst ψ.left, snd := whiskerRight (𝟙 X✝).snd ψ.right, w := ⋯ }.fst.app x✝ =
    (𝟙
            { fst := X✝.fst ⋙ ψ.left, snd := X✝.snd ⋙ ψ.right,
              iso :=
                X✝.fst.associator ψ.left F₁ ≪≫
                  X✝.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (X✝.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight X✝.iso ψ.base ≪≫
                        X✝.snd.associator G ψ.base ≪≫
                          X✝.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (X✝.snd.associator ψ.right G₁).symm }).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
ψ : CatCospanTransform F G F₁ G₁
X✝ : CatCommSqOver F G X
x✝ : X
⊢ { fst := whiskerRight (𝟙 X✝).fst ψ.left, snd := whiskerRight (𝟙 X✝).snd ψ.right, w := ⋯ }.snd.app x✝ =
    (𝟙
            { fst := X✝.fst ⋙ ψ.left, snd := X✝.snd ⋙ ψ.right,
              iso :=
                X✝.fst.associator ψ.left F₁ ≪≫
                  X✝.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (X✝.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight X✝.iso ψ.base ≪≫
                        X✝.snd.associator G ψ.base ≪≫
                          X✝.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (X✝.snd.associator ψ.right G₁).symm }).snd.app
      x✝