∀ {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₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  (pt : C₃) (inl : (F.obj Y₁).obj X₂ ⟶ pt) (inr : (F.obj X₁).obj Y₂ ⟶ pt)
  (isPushout : CategoryTheory.IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) inl inr) (pt_1 : C₃)
  (inl_1 : (F.obj Y₁).obj X₂ ⟶ pt_1) (inr_1 : (F.obj X₁).obj Y₂ ⟶ pt_1)
  (isPushout_1 : CategoryTheory.IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) inl_1 inr_1),
  ({ pt := pt, inl := inl, inr := inr, isPushout := isPushout } =
      { pt := pt_1, inl := inl_1, inr := inr_1, isPushout := isPushout_1 }) =
    (pt = pt_1 ∧ inl ≍ inl_1 ∧ inr ≍ inr_1)