∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {J : Type}
  [inst_2 : Fintype J] {f : J → C} [inst_3 : CategoryTheory.Limits.HasBiproduct f] {T U : C} {g : (j : J) → T ⟶ f j}
  {h : (j : J) → f j ⟶ U} {Z : C} (h_1 : U ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc h) h_1) =
    CategoryTheory.CategoryStruct.comp (∑ j, CategoryTheory.CategoryStruct.comp (g j) (h j)) h_1