-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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₁
A₂ : Type u₇
B₂ : Type u₈
C₂ : Type u₉
inst_6 : Category.{v₇, u₇} A₂
inst_7 : Category.{v₈, u₈} B₂
inst_8 : 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₁₁
inst_9 : Category.{v₁₀, u₁₀} X
inst_10 : Category.{v₁₁, u₁₁} Y
U : Functor.{v₁₀, v₁₁, u₁₀, u₁₁} X Y
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₁₁, u₁, u₂, u₃, u₁₁} F G Y) (x_1 : X),
    NatTrans.app
        (Hom.fst
          (NatTrans.app
            (Iso.hom
                (CatCommSq.iso (obj (transform Y) (ψ.comp ψ')) (obj (precompose F G) U) (obj (precompose F₂ G₂) U)
                  (obj (transform X) (ψ.comp ψ'))) ≫
              (obj (precompose F G) U).whiskerLeft (Iso.hom (transformObjComp X ψ ψ')))
            x))
        x_1 =
      NatTrans.app
        ((whiskerRight (Iso.hom (transformObjComp Y ψ ψ')) (obj (precompose F₂ G₂) U) ≫
                Iso.hom (associator (obj (transform Y) ψ) (obj (transform Y) ψ') (obj (precompose F₂ G₂) U)) ≫
                  whiskerLeft (obj (transform Y) ψ)
                      (Iso.hom
                        (CatCommSq.iso (obj (transform Y) ψ') (obj (precompose F₁ G₁) U) (obj (precompose F₂ G₂) U)
                          (obj (transform X) ψ'))) ≫
                    Iso.inv (associator (obj (transform Y) ψ) (obj (precompose F₁ G₁) U) (obj (transform X) ψ')) ≫
                      whiskerRight
                          (Iso.hom
                            (CatCommSq.iso (obj (transform Y) ψ) (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
                              (obj (transform X) ψ)))
                          (obj (transform X) ψ') ≫
                        ((obj (precompose F G) U).associator (obj (transform X) ψ) (obj (transform X) ψ')).hom).app
            x).fst
        x_1
⊢ Iso.hom
        (CatCommSq.iso (obj (transform Y) (ψ.comp ψ')) (obj (precompose F G) U) (obj (precompose F₂ G₂) U)
          (obj (transform X) (ψ.comp ψ'))) ≫
      (obj (precompose F G) U).whiskerLeft (Iso.hom (transformObjComp X ψ ψ')) =
    whiskerRight (Iso.hom (transformObjComp Y ψ ψ')) (obj (precompose F₂ G₂) U) ≫
      Iso.hom (associator (obj (transform Y) ψ) (obj (transform Y) ψ') (obj (precompose F₂ G₂) U)) ≫
        whiskerLeft (obj (transform Y) ψ)
            (Iso.hom
              (CatCommSq.iso (obj (transform Y) ψ') (obj (precompose F₁ G₁) U) (obj (precompose F₂ G₂) U)
                (obj (transform X) ψ'))) ≫
          Iso.inv (associator (obj (transform Y) ψ) (obj (precompose F₁ G₁) U) (obj (transform X) ψ')) ≫
            whiskerRight
                (Iso.hom
                  (CatCommSq.iso (obj (transform Y) ψ) (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
                    (obj (transform X) ψ)))
                (obj (transform X) ψ') ≫
              ((obj (precompose F G) U).associator (obj (transform X) ψ) (obj (transform X) ψ')).hom
have w₁ : ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₁₁, u₁, u₂, u₃, u₁₁} F G Y) (x_1 : X),
  NatTrans.app
      (Hom.snd
        (NatTrans.app
          (Iso.hom
              (CatCommSq.iso (obj (transform Y) (ψ.comp ψ')) (obj (precompose F G) U) (obj (precompose F₂ G₂) U)
                (obj (transform X) (ψ.comp ψ'))) ≫
            (obj (precompose F G) U).whiskerLeft (Iso.hom (transformObjComp X ψ ψ')))
          x))
      x_1 =
    NatTrans.app
      ((whiskerRight (Iso.hom (transformObjComp Y ψ ψ')) (obj (precompose F₂ G₂) U) ≫
              Iso.hom (associator (obj (transform Y) ψ) (obj (transform Y) ψ') (obj (precompose F₂ G₂) U)) ≫
                whiskerLeft (obj (transform Y) ψ)
                    (Iso.hom
                      (CatCommSq.iso (obj (transform Y) ψ') (obj (precompose F₁ G₁) U) (obj (precompose F₂ G₂) U)
                        (obj (transform X) ψ'))) ≫
                  Iso.inv (associator (obj (transform Y) ψ) (obj (precompose F₁ G₁) U) (obj (transform X) ψ')) ≫
                    whiskerRight
                        (Iso.hom
                          (CatCommSq.iso (obj (transform Y) ψ) (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
                            (obj (transform X) ψ)))
                        (obj (transform X) ψ') ≫
                      ((obj (precompose F G) U).associator (obj (transform X) ψ) (obj (transform X) ψ')).hom).app
          x).snd
      x_1
Tactic: ext