∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} (pt : C₂) (fst : pt ⟶ (G.obj (Opposite.op X₁)).obj X₃) (snd : pt ⟶ (G.obj (Opposite.op Y₁)).obj Y₃)
  (isPullback : CategoryTheory.IsPullback fst snd ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)) (pt_1 : C₂)
  (fst_1 : pt_1 ⟶ (G.obj (Opposite.op X₁)).obj X₃) (snd_1 : pt_1 ⟶ (G.obj (Opposite.op Y₁)).obj Y₃)
  (isPullback_1 : CategoryTheory.IsPullback fst_1 snd_1 ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)),
  ({ pt := pt, fst := fst, snd := snd, isPullback := isPullback } =
      { pt := pt_1, fst := fst_1, snd := snd_1, isPullback := isPullback_1 }) =
    (pt = pt_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1)