Lean: Indecomposable depends on the HasBinaryBiproducts instance; prove it doesn't

Mathlib's CategoryTheory.Indecomposable X takes [HasBinaryBiproducts C] as an instance argument, so the same statement elaborated in two contexts (e.g. one using hasBinaryBiproducts_of_finite_biproducts as a local instance, another using whatever the category provides, as in FGModuleCat R or a pretriangulated category) gives terms that are not defeq, and rw/exact fail with confusing mismatches. Fix once with a congruence lemma: lemma indecomposable_iff_of_hasBinaryBiproducts [HasZeroMorphisms C] (h₁ h₂ : HasBinaryBiproducts C) (X : C) : @Indecomposable C _ _ h₁ X ↔ @Indecomposable C _ _ h₂ X. Proof: compose the given iso X ≅ Y ⊞ Z with @biprod.uniqueUpToIso _ _ _ Y Z (h₁.1 Y Z) _ (@BinaryBiproduct.isBilimit _ _ _ Y Z (h₂.1 Y Z)) in both directions. Use it as indecomposable_iff_of_hasBinaryBiproducts _ inferInstance (rw needs the second instance supplied explicitly). Design tip: when you write a class about indecomposables, take [HasBinaryBiproducts C] as its own parameter next to [HasFiniteBiproducts C] instead of deriving it locally, so applications pick up the ambient instance. Related: FGModuleCat R needs a manual HasFiniteBiproducts := .of_hasFiniteProducts, forget₂ (FGModuleCat R) (ModuleCat R) needs have := preservesBinaryBiproducts_of_preservesBiproducts (forget₂ ..) before mapBiprod, and the underlying module of ⨁ f is ((forget₂ ..).mapBiproduct f ≪≫ ModuleCat.biproductIsoPi _).toLinearEquiv. Write ((⨁ f) : FGModuleCat R) in parentheses; (⨁ f : T) is parsed as a binder ascription.