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 y : CatCommSqOver F G X
f : x ⟶ y
⊢ whiskerRight (whiskerRight f.fst ψ.left) F₁ ≫
      { fst := y.fst ⋙ ψ.left, snd := y.snd ⋙ ψ.right,
            iso :=
              y.fst.associator ψ.left F₁ ≪≫
                y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (y.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight y.iso ψ.base ≪≫
                      y.snd.associator G ψ.base ≪≫
                        y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                          (y.snd.associator ψ.right G₁).symm }.iso.hom =
    { 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 }.iso.hom ≫
      whiskerRight (whiskerRight f.snd ψ.right) G₁

Tactic:
ext x

Goal state after:
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✝ y : CatCommSqOver F G X
f : x✝ ⟶ y
x : X
⊢ (whiskerRight (whiskerRight f.fst ψ.left) F₁ ≫
          { fst := y.fst ⋙ ψ.left, snd := y.snd ⋙ ψ.right,
                iso :=
                  y.fst.associator ψ.left F₁ ≪≫
                    y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                      (y.fst.associator F ψ.base).symm ≪≫
                        isoWhiskerRight y.iso ψ.base ≪≫
                          y.snd.associator G ψ.base ≪≫
                            y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                              (y.snd.associator ψ.right G₁).symm }.iso.hom).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 }.iso.hom ≫
          whiskerRight (whiskerRight f.snd ψ.right) G₁).app
      x