∀ {J : Type u_4} {K : Type u_3} {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f] [inst_3 : CategoryTheory.Limits.HasBiproduct g],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.desc fun k =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
          (CategoryTheory.CategoryStruct.comp (w (e.symm k)).hom (CategoryTheory.Limits.biproduct.ι f (e.symm k))))
      (CategoryTheory.Limits.biproduct.desc fun j =>
        CategoryTheory.CategoryStruct.comp (w j).inv (CategoryTheory.Limits.biproduct.ι g (e j))) =
    CategoryTheory.CategoryStruct.id (⨁ g)