Commit 2023-04-28 06:22 a5ff45a1

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.