∀ {A : Type u_3} {B : Type u_6} {C : Type u_4} [inst : CategoryTheory.Category.{u_1, u_3} A]
  [inst_1 : CategoryTheory.Category.{u_5, u_6} B] [inst_2 : CategoryTheory.Category.{u_2, u_4} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (eₗ : x.fst ≅ y.fst) (eᵣ : x.snd ≅ y.snd)
  (w :
    CategoryTheory.CategoryStruct.comp (F.map eₗ.hom) y.iso.hom =
      CategoryTheory.CategoryStruct.comp x.iso.hom (G.map eᵣ.hom)),
  CategoryTheory.CategoryStruct.comp { fst := eₗ.hom, snd := eᵣ.hom, w := w } { fst := eₗ.inv, snd := eᵣ.inv, w := ⋯ } =
    CategoryTheory.CategoryStruct.id x