∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {X' Y' : C}
  (c : CategoryTheory.Limits.Cofork f g) (hc hc_1 : CategoryTheory.Limits.IsColimit c),
  hc = hc_1 →
    ∀ {f' g' : X' ⟶ Y'} (c' : CategoryTheory.Limits.Cofork f' g') (e₀ e₀_1 : X ≅ X') (e_e₀ : e₀ = e₀_1)
      (e₁ e₁_1 : Y ≅ Y') (e_e₁ : e₁ = e₁_1) (e e_1 : c.pt ≅ c'.pt) (e_e : e = e_1)
      (comm₁ : CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom)
      (comm₂ : CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom)
      (comm₃ : CategoryTheory.CategoryStruct.comp e₁.inv (CategoryTheory.CategoryStruct.comp c.π e.hom) = c'.π),
      c.isColimitOfIsos hc c' e₀ e₁ e comm₁ comm₂ comm₃ = c.isColimitOfIsos hc_1 c' e₀_1 e₁_1 e_1 ⋯ ⋯ ⋯