The Quillen-Suslin Theorem

Formalizing the following Quillen-Suslin theorem in Lean:

Any finitely generated projective module over the $R[x_1, \dots, x_n]$ is free, where $R$ is a principal ideal domain.