-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst_3 : Category.{v₄, u₄} A₁
inst_4 : Category.{v₅, u₅} B₁
inst_5 : Category.{v₆, u₆} C₁
F₁ : Functor.{v₄, v₅, u₄, u₅} A₁ B₁
G₁ : Functor.{v₆, v₅, u₆, u₅} C₁ B₁
X : Type u₇
Y : Type u₈
Z : Type u₉
inst_6 : Category.{v₇, u₇} X
inst_7 : Category.{v₈, u₈} Y
inst_8 : Category.{v₉, u₉} Z
ψ : CatCospanTransform F G F₁ G₁
U : Functor.{v₇, v₈, u₇, u₈} X Y
V : Functor.{v₈, v₉, u₈, u₉} Y Z
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₉, u₁, u₂, u₃, u₉} F G Z) (x_1 : X),
    ((Iso.hom
                    (CatCommSq.iso (obj (precompose F G) (U ⋙ V)) (obj (transform Z) ψ) (obj (transform X) ψ)
                      (obj (precompose F₁ G₁) (U ⋙ V))) ≫
                  whiskerLeft (obj (transform Z) ψ) (precomposeObjComp F₁ G₁ U V).hom).app
              x).fst.app
        x_1 =
      NatTrans.app
        (Hom.fst
          ((whiskerRight (precomposeObjComp F G U V).hom (obj (transform X) ψ) ≫
                ((obj (precompose F G) V).associator (obj (precompose F G) U) (obj (transform X) ψ)).hom ≫
                  (obj (precompose F G) V).whiskerLeft
                      (Iso.hom
                        (CatCommSq.iso (obj (precompose F G) U) (obj (transform Y) ψ) (obj (transform X) ψ)
                          (obj (precompose F₁ G₁) U))) ≫
                    ((obj (precompose F G) V).associator (obj (transform Y) ψ) (obj (precompose F₁ G₁) U)).inv ≫
                      whiskerRight
                          (Iso.hom
                            (CatCommSq.iso (obj (precompose F G) V) (obj (transform Z) ψ) (obj (transform Y) ψ)
                              (obj (precompose F₁ G₁) V)))
                          (obj (precompose F₁ G₁) U) ≫
                        Iso.hom
                          (associator (obj (transform Z) ψ) (obj (precompose F₁ G₁) V) (obj (precompose F₁ G₁) U))).app
            x))
        x_1
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₉, u₁, u₂, u₃, u₉} F G Z) (x_1 : X),
    ((Iso.hom
                    (CatCommSq.iso (obj (precompose F G) (U ⋙ V)) (obj (transform Z) ψ) (obj (transform X) ψ)
                      (obj (precompose F₁ G₁) (U ⋙ V))) ≫
                  whiskerLeft (obj (transform Z) ψ) (precomposeObjComp F₁ G₁ U V).hom).app
              x).snd.app
        x_1 =
      NatTrans.app
        (Hom.snd
          ((whiskerRight (precomposeObjComp F G U V).hom (obj (transform X) ψ) ≫
                ((obj (precompose F G) V).associator (obj (precompose F G) U) (obj (transform X) ψ)).hom ≫
                  (obj (precompose F G) V).whiskerLeft
                      (Iso.hom
                        (CatCommSq.iso (obj (precompose F G) U) (obj (transform Y) ψ) (obj (transform X) ψ)
                          (obj (precompose F₁ G₁) U))) ≫
                    ((obj (precompose F G) V).associator (obj (transform Y) ψ) (obj (precompose F₁ G₁) U)).inv ≫
                      whiskerRight
                          (Iso.hom
                            (CatCommSq.iso (obj (precompose F G) V) (obj (transform Z) ψ) (obj (transform Y) ψ)
                              (obj (precompose F₁ G₁) V)))
                          (obj (precompose F₁ G₁) U) ≫
                        Iso.hom
                          (associator (obj (transform Z) ψ) (obj (precompose F₁ G₁) V) (obj (precompose F₁ G₁) U))).app
            x))
        x_1
⊢ Iso.hom
        (CatCommSq.iso (obj (precompose F G) (U ⋙ V)) (obj (transform Z) ψ) (obj (transform X) ψ)
          (obj (precompose F₁ G₁) (U ⋙ V))) ≫
      whiskerLeft (obj (transform Z) ψ) (precomposeObjComp F₁ G₁ U V).hom =
    whiskerRight (precomposeObjComp F G U V).hom (obj (transform X) ψ) ≫
      ((obj (precompose F G) V).associator (obj (precompose F G) U) (obj (transform X) ψ)).hom ≫
        (obj (precompose F G) V).whiskerLeft
            (Iso.hom
              (CatCommSq.iso (obj (precompose F G) U) (obj (transform Y) ψ) (obj (transform X) ψ)
                (obj (precompose F₁ G₁) U))) ≫
          ((obj (precompose F G) V).associator (obj (transform Y) ψ) (obj (precompose F₁ G₁) U)).inv ≫
            whiskerRight
                (Iso.hom
                  (CatCommSq.iso (obj (precompose F G) V) (obj (transform Z) ψ) (obj (transform Y) ψ)
                    (obj (precompose F₁ G₁) V)))
                (obj (precompose F₁ G₁) U) ≫
              Iso.hom (associator (obj (transform Z) ψ) (obj (precompose F₁ G₁) V) (obj (precompose F₁ G₁) U))

Tactic:
ext