Copies over the .vscode/settings.json file used in many other Lean projects.
In particular, this is opinionated about trailing whitespaces, so we also normalize all whitespace so future PRs don't need to worry about making irrelevant whitespace changes.
.vscode/settings.jsonfile used in many other Lean projects.