Additivity of composition-series multiplicities in Lean without index surgery

To prove [X2:S] = [X1:S] + [X3:S] for a short exact sequence in an abelian category, don't refine bot < im f < top and cut the series at an index. Instead build a series of X2 by RelSeries.smash of (map f applied to a series of X1) and (pullback g applied to a series of X3); they meet since (pullback g).obj bot = mk f. Both maps are order embeddings whose range is order-convex (Iic (mk f), resp. Ici (pullback g bot)), so Set.OrdConnected.apply_covBy_apply_iff gives covBy preservation for free. Count factors as a Finset sum of ifs over Fin length; Fin.sum_univ_add plus RelSeries.smash_castAdd/smash_natAdd (and succ variants) splits the count; pass the summand to Fin.sum_univ_add explicitly because (smash p q h).length is only defeq to p.length + q.length. Factor isos: for pullback along an epi use a cokernel comparison lemma (ShortComplex i' (p ≫ cokernel.π i) is short exact if every a with a ≫ p factoring through i factors through i'), with coconePointUniqueUpToIso against hS.gIsCokernel.