∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} A}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {inst_2 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  {inst_3 : CategoryTheory.Category.{v₄, u₄} X} {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  {fst : x.fst ⟶ y.fst} {snd : x.snd ⟶ y.snd}
  {w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight fst F) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight snd G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w._autoParam}
  {fst_1 : x.fst ⟶ y.fst} {snd_1 : x.snd ⟶ y.snd}
  {w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight fst_1 F) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight snd_1 G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w._autoParam},
  { fst := fst, snd := snd, w := w } = { fst := fst_1, snd := snd_1, w := w_1 } → fst = fst_1 ∧ snd = snd_1