chore(category_theory/abelian): backport removal of abelian.has_finit…

…e_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~~ leanprover/lean4#2055 during the simpNF linter in leanprover-community/mathlib4#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>

src/category_theory/abelian/basic.lean

@@ -257,10 +257,15 @@ namespace category_theory.abelian
 variables {C : Type u} [category.{v} C] [abelian C]
 
 /-- An abelian category has finite biproducts. -/
-@[priority 100]
-instance has_finite_biproducts : has_finite_biproducts C :=
+-- Porting note: this should be an instance,
+-- but triggers https://github.com/leanprover/lean4/issues/2055
+-- We set it as a local instance instead.
+-- @[priority 100] instance
+theorem has_finite_biproducts : has_finite_biproducts C :=
 limits.has_finite_biproducts.of_has_finite_products
 
+local attribute [instance] has_finite_biproducts
+
 @[priority 100]
 instance has_binary_biproducts : has_binary_biproducts C :=
 limits.has_binary_biproducts_of_finite_biproducts _

src/category_theory/abelian/opposite.lean

@@ -25,6 +25,11 @@ variables (C : Type*) [category C] [abelian C]
 local attribute [instance]
   has_finite_limits_of_has_equalizers_and_finite_products
   has_finite_colimits_of_has_coequalizers_and_finite_coproducts
+  -- Porting note:
+  -- This should have been a global instance,
+  -- but triggers https://github.com/leanprover/lean4/issues/2055
+  -- when ported to mathlib4.
+  abelian.has_finite_biproducts
 
 instance : abelian Cᵒᵖ :=
 { normal_mono_of_mono := λ X Y f m, by exactI