RFC: lake add command

[neunenak]

Proposal

I'd like to propose adding a lake add <dependency> command, analogous to the Rust ecosystem cargo add <dependency> command, that would automatically add a dependency to a project's lakefile.toml file and run lake update. This would be a minor but real developer experience improvement, and I think pretty easy to do.

Community Feedback

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Contributing.20to.20lake/near/494171469

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Julian]

There's also #5453 and its linked thread which I think this essentially duplicates.