Mathlib: make a Serre class an abelian full subcategory (missing finite-products instance)

Mathlib's Abelian/Subcategory.lean gives Abelian P.FullSubcategory from ContainsZero + IsClosedUnderKernels + IsClosedUnderCokernels + IsClosedUnderFiniteProducts, and the first three follow from IsSerreClass by instances, but IsClosedUnderFiniteProducts does not. Supply IsClosedUnderBinaryProducts (= IsClosedUnderLimitsOfShape (Discrete WalkingPair)): take the LimitOfShape presentation p, show P (X₁ ⊞ X₂) via P.prop_X₂_of_shortExact (ShortComplex.Splitting.ofHasBinaryBiproduct X₁ X₂).shortExact, then transport along biprod.isoProd _ _ ≪≫ IsLimit.conePointUniqueUpToIso (prodIsProd _ _) ((IsLimit.postcomposeHomEquiv (diagramIsoPair p.diag) _).2 p.isLimit); then instance : P.IsClosedUnderFiniteProducts := .mk' (empty case is an existing instance). Exactness of P.ι: rw [((Functor.preservesFiniteLimits_tfae P.ι).out 4 3 :)]; intro _ _ f; exact P.preservesKernels_ι f (tfae lives in Algebra/Homology/ShortComplex/ExactFunctor.lean), dually with preservesCokernels_ι.