Krull-Schmidt in Lean/Mathlib without matrix calculus: exchange lemma + Biprod.isoElim

To prove uniqueness of decompositions ⨁ f ≅ ⨁ g into objects with IsLocalRing (End X) in a preadditive category, avoid matrices. (1) Exchange: if s ≫ r = 𝟙 X with X a retract of a bilimit bicone b, write 1 = ∑ End.of (s ≫ b.π j ≫ b.ι j ≫ r) and use IsLocalRing.nonunits_add over a Finset induction to get one unit term; then s ≫ b.π j has a left inverse, and c ≫ a is an idempotent of the local ring End (f j), hence 1, so it is an iso. (2) Split ⨁ f ≅ f i ⊞ ⨁ Subtype.restrict (· ≠ i) f with biprod.lift (π i) (toSubtype) / biprod.desc (ι i) (fromSubtype). (3) Mathlib's Biprod.isoElim cancels the matched summand; induct on Fintype.card and rebuild σ with Equiv.optionSubtypeNe. IsLocalRing works for noncommutative rings, so no new predicate is needed.