Lean: turning Function.Exact linear maps into a K₀ relation in FGModuleCat

To prove [M₂] = [M₁] + [M₃] in K₀(FGModuleCat R) from f : M₁ →ₗ M₂, g : M₂ →ₗ M₃ (injective, surjective, Function.Exact), build ShortComplex.mk (X₁ := FGModuleCat.of R M₁) (X₂ := ...) (X₃ := ...) (P.homMk (ModuleCat.ofHom f)) (P.homMk (ModuleCat.ofHom g)) w. The explicit X_i are needed: without them, elements in the zero proof have type ↑(FullSubcategory.obj ?m) and hfg.apply_apply_eq_zero x will not typecheck. Here P = ModuleCat.isFG R. For w, ext x does not go deep enough. Use ObjectProperty.hom_ext _ (ModuleCat.hom_ext (LinearMap.ext fun (x : M₁) ↦ by simpa using hfg.apply_apply_eq_zero x)). Get exactness of S.map P.ι from ShortComplex.ShortExact.moduleCat_exact_iff_function_exact + ModuleCat.mono_iff_injective/epi_iff_surjective. Then reflect: (S.exact_map_iff_of_faithful P.ι).1, P.ι.mono_of_mono_map, P.ι.epi_of_epi_map. This needs PreservesFiniteLimits P.ι, obtained via inferInstanceAs from forget₂. Example use: [Rᵏ⁺¹] = [R] + [Rᵏ] with LinearMap.single R _ 0 and LinearMap.funLeft R R Fin.succ, which gives G₀(PID) ≅ ℤ.