-- 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₁₀
inst_9 : Category.{v₁₀, u₁₀} X
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x y : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X
f : x ⟶ y
h₁ :
  ∀ (x_1 : X),
    Eq (α :=
      (obj (obj (transform X) (ψ.comp ψ')) x).fst.obj x_1 ⟶
        (obj (obj (transform X) ψ ⋙ obj (transform X) ψ') y).fst.obj x_1)
      (NatTrans.app
        (Hom.fst
          (map (obj (transform X) (ψ.comp ψ')) f ≫
            Iso.hom
              ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X) ↦
                  (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯ :
                    obj (obj (transform X) (ψ.comp ψ')) x ≅ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') x))
                y)))
        x_1)
      (NatTrans.app
        (Hom.fst
          (Iso.hom
              ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X) ↦
                  (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯ :
                    obj (obj (transform X) (ψ.comp ψ')) x ≅ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') x))
                x) ≫
            map (obj (transform X) ψ ⋙ obj (transform X) ψ') f))
        x_1)
⊢ Eq (α := obj (obj (transform X) (ψ.comp ψ')) x ⟶ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') y)
    (map (obj (transform X) (ψ.comp ψ')) f ≫
      Iso.hom
        ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X) ↦
            (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯ :
              obj (obj (transform X) (ψ.comp ψ')) x ≅ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') x))
          y))
    (Iso.hom
        ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X) ↦
            (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯ :
              obj (obj (transform X) (ψ.comp ψ')) x ≅ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') x))
          x) ≫
      map (obj (transform X) ψ ⋙ obj (transform X) ψ') f)
have h₂ : ∀ (x_1 : X),
  Eq (α :=
    (obj (obj (transform X) (ψ.comp ψ')) x).snd.obj x_1 ⟶
      (obj (obj (transform X) ψ ⋙ obj (transform X) ψ') y).snd.obj x_1)
    (NatTrans.app
      (Hom.snd
        (map (obj (transform X) (ψ.comp ψ')) f ≫
          Iso.hom
            ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X) ↦
                (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm sorry :
                  obj (obj (transform X) (ψ.comp ψ')) x ≅ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') x))
              y)))
      x_1)
    (NatTrans.app
      (Hom.snd
        (Iso.hom
            ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X) ↦
                (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm sorry :
                  obj (obj (transform X) (ψ.comp ψ')) x ≅ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') x))
              x) ≫
          map (obj (transform X) ψ ⋙ obj (transform X) ψ') f))
      x_1)
Tactic: ext