`lake new` should generate a `lakefile.toml`, not a `lakefile.lean`

[semorrison]

Going forward, I hope we can think of lakefile.lean as a feature for expert users, who have complicated requirements, and that most people can and should be using a lakefile.toml.

With that in mind, I think lake new and lake init should create a toml.

(I think it would not be a bad idea for that toml to contain a comment line to the effect. "If you need dynamic features only possible with a lakefile.lean , use lake translate-config lean to convert this lakefile.toml into a lakefile.lean.")