∀ {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 sq.cokernelCofork)
  (s : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.biprod.lift f (-g)) 0) (m : sq.cokernelCofork.pt ⟶ s.pt),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π sq.cokernelCofork) m = s.π →
    m =
      CategoryTheory.Limits.PushoutCocone.IsColimit.desc
        (CategoryTheory.Limits.PushoutCocone.IsColimit.mk ⋯
          (fun s => x.desc (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biprod.desc s.inl s.inr) ⋯))
          ⋯ ⋯ ⋯)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl s.π)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr s.π) ⋯