∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{u_1, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive]
  (X : CategoryTheory.Mat_ C),
  (CategoryTheory.Limits.biproduct.matrix fun i j => F.map (CategoryTheory.CategoryStruct.id X i j)) =
    CategoryTheory.CategoryStruct.id (⨁ fun i => F.obj (X.X i))