∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq f g inl inr)
  (x : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr ⋯))
  (s : CategoryTheory.Limits.PushoutCocone f g) (m : X₄ ⟶ s.pt),
  CategoryTheory.CategoryStruct.comp inl m = s.inl →
    CategoryTheory.CategoryStruct.comp inr m = s.inr →
      m =
        (CategoryTheory.Limits.Cofork.IsColimit.mk sq.cokernelCofork
              (fun s =>
                CategoryTheory.Limits.PushoutCocone.IsColimit.desc x
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl s.π)
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr s.π) ⋯)
              ⋯ ⋯).desc
          (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biprod.desc s.inl s.inr) ⋯)