doc: how to depend on the library (#513)

Co-authored-by: Joe Hendrix <[email protected]>
Co-authored-by: François G. Dorais <[email protected]>

README.md

@@ -2,6 +2,16 @@
 
 Work in progress standard library for Lean 4. This is a collection of data structures and tactics intended for use by both computer-science applications and mathematics applications of Lean 4.
 
+# Using `std4`
+
+To use `std4` in your project, add the following to your `lakefile.lean`:
+
+```lean
+require std from git "https://github.com/leanprover/std4" @ "main"
+```
+
+Additionally, please make sure that you're using the version of Lean that the current version of `std4` expects. The easiest way to do this is to copy the [`lean-toolchain`](./lean-toolchain) file from this repository to your project. Once you've added the dependency declaration, the command `lake update` checks out the current version of `std4` and writes it the Lake manifest file. Don't run this command again unless you're prepared to potentially also update your Lean compiler version, as it will retrieve the latest version of dependencies and add them to the manifest.
+
 # Build instructions
 
 * Get the newest version of `elan`. If you already have installed a version of Lean, you can run