mathlib3

a5ff45a1 - chore(category_theory/abelian): backport removal of abelian.has_finite_biproducts instance (#18740)

chore(category_theory/abelian): backport removal of abelian.has_finite_biproducts instance (#18740) This backports a proposed removal of the `abelian.has_finite_biproducts` global instance, instead enabling it locally in the files that need it. The reason for removing it is that it triggers the ~~dreaded~~ https://github.com/leanprover/lean4/issues/2055 during the simpNF linter in https://github.com/leanprover-community/mathlib4/pull/2769, the mathlib4 port of `category_theory.abelian.basic`. This backport verifies that we won't run into further problems downstream if we (hopefully temporarily) remove these instances in mathlib4. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>