The Stacks project

I recently formalized this lemmas in Lean, and was able to weaken the locally free assumption to flatness. The proof ends up like this: to show that $x_1,\dots,x_d$ is a basis amounts to showing the induced map $R^n\to M$ is bijective, for which it suffices to show ${R_\mathfrak{m}}^n\to M_\mathfrak{m}$ is bijective for each maximal $\mathfrak{m}$. (This is completed using bijective_of_localized_maximal in Lean; I'm not sure whether the counterparts of the surrounding lemmas exist in Stacks.) Since $M_\mathfrak{m}$ is finite flat over the local ring $R_\mathfrak{m}$, from the proof of 00NZ, it suffices to show $(R_\mathfrak{m}/\mathfrak{m}R_\mathfrak{m})^n \to M_\mathfrak{m}/\mathfrak{m}M_\mathfrak{m}$ is bijective, but this map is the base change of $(R/\mathfrak{m})^n\to M/\mathfrak{m}M$, which is bijective by choice of the $x_i$.

(In Lean the argument is all carried out using tensor products: localizations and quotients of $M$ doesn't appear, only the tensor product of $M$ with localizations and quotients of $R$. There doesn't seem to be a statement of CRT for modules in Stacks, but of course one can just tensor the surjection $R\to\prod_\mathfrak{m}R/\mathfrak{m}$ with $M$.)

A direct consequence of this lemma is that the Picard group of a semi-local ring is trivial. Combined with the observation that a Noetherian total ring of fraction must be semi-local, one can deduce that invertible modules over Noetherian rings are isomorphic to ideals: This has also been formalized in Lean.