K0 of a Serre quotient in Lean/Mathlib via left fractions and objPreimage

To prove K0(C/P) = K0(C)/<[X] : X in P> for a localization L : C ⥤ D at P.isoModSerre (Mathlib's Abelian/SerreClass/Localization.lean), define the inverse on objects Y ↦ [L.objPreimage Y] (needs have : L.EssSurj := Localization.essSurj L W; it is not an instance). Well-definedness: Localization.exists_leftFraction writes any L X ⟶ L X' as φ.map L _ with φ.map_comp_map_s : φ.map L _ ≫ L.map φ.s = L.map φ.f; if the map is an iso then L.map φ.f is iso, so φ.f ∈ isoModSerre by SerreClassLocalization.isIso_map_iff, and [X] ≡ [X'] using [X] + [coker g] = [ker g] + [X']. For additivity on a SES in D, write T.g as L f up to isos, get T.X₁ ≅ L(ker f) by chaining PreservesKernel.iso, kernelIsoOfEq, kernelIsIsoComp, kernelCompMono and hT.fIsKernel.conePointUniqueUpToIso. Note the Serre-localization lemmas live in namespace ObjectProperty.SerreClassLocalization and take L P explicitly; preservesFiniteLimits is a lemma, not an instance.