diff --git a/docs/INSTALLATION.md b/docs/INSTALLATION.md
index cd03de1..1eecc7f 100644
--- a/docs/INSTALLATION.md
+++ b/docs/INSTALLATION.md
@@ -2,14 +2,4 @@
 
 You can install Lean by following the [installation instructions][install] on the official website.
 
-The recommended way to install Lean is through **Visual Studio Code** and the **Lean 4 VS Code** extension.
-This extension automatically installs all required dependencies.
-It also includes syntax highlighting, code completion, version management, links to learning resources and documentation, and many other useful tools.
-
-There are also alternative methods for [manual installation][manual-install], with support for some other editors.
-
-You can also try out the language on the official [web playground][playground] without installing anything.
-
-[install]: https://lean-lang.org/install/
-[manual-install]: https://lean-lang.org/install/manual/
-[playground]: https://live.lean-lang.org/
+[install]: https://lean-lang.org/instal
diff --git a/docs/LEARNING.md b/docs/LEARNING.md
index 5dea330..6df2b8f 100644
--- a/docs/LEARNING.md
+++ b/docs/LEARNING.md
@@ -10,7 +10,7 @@ For a more in-depth look at theorem proving in Lean, the book [Theorem Proving i
 
 [The Lean Language Reference][lean-reference] is the authoritative source for detailed information about the language.
 
-Many additional resources for learning Lean are made available by the community in [this repository][community-resources].
+Many additional resources for learning Lean are made available by the [Lean Community][community-resources].
 
 [community-resources]: https://leanprover-community.github.io/learn.html
 [functional-programming]: https://lean-lang.org/functional_programming_in_lean/
diff --git a/docs/RESOURCES.md b/docs/RESOURCES.md
index dff9476..13a565f 100644
--- a/docs/RESOURCES.md
+++ b/docs/RESOURCES.md
@@ -1,6 +1,7 @@
 # Resources
 
 * The [official site][lean-lang] is the main repository for content about the language.
+  It has an online [playground][playground] where you can try out the language without installing anything.
 * The [Reservoir][reservoir] indexes, builds and tests packages within the Lean and Lake ecosystem.
   It is the place to go for third-party packages.
 * [Lean Community][community] is a collaborative, open-source network around the Lean ecosystem.
@@ -8,6 +9,7 @@
 * [Lean 4 Zulip Chat][zulip-chat] is the main chat for the Lean Community.
 
 [lean-lang]: https://lean-lang.org/
+[playground]: https://live.lean-lang.org/
 [reservoir]: https://reservoir.lean-lang.org/
 [community]: https://leanprover-community.github.io/index.html
 [zulip-chat]: https://leanprover.zulipchat.com/
diff --git a/docs/TESTS.md b/docs/TESTS.md
index b5aced6..b23fd9a 100644
--- a/docs/TESTS.md
+++ b/docs/TESTS.md
@@ -51,7 +51,7 @@ All of them are expected to be defined in the solution module, within a namespac
 Each argument and the return value for each function has some type.
 This might be one of the basic types in Lean (for example, `Nat`, `List Int` or `Option String`), or a user-defined type.
 
-You'll a find a file with the correct name already in place in the same folder as the test module.
+You will find a file with the correct name already in place in the same folder as the test module.
 This file should have a _stub_ with most initial informations, so that you can use it as a starting point for your solution.
 
 Just keep in mind that this stub is there just for you to get started. 
@@ -59,8 +59,8 @@ Feel free to change it completely if you think it is the right thing to do.
 
 ## Using packages
 
-Lean projects using Lake may always import the standard library `Std`, which contains additional data structures, IO and system APIs, and other basic utilities.
-This import should be at the beggining of the file:
+Lean projects using Lake may always import the standard library `Std`, which contains additional data structures, I/O and system APIs, and other basic utilities.
+This import should be at the beginning of the file:
 
 ```lean
 import Std
@@ -68,8 +68,10 @@ import Std
 def someMap : Std.HashMap Int Nat := ...
 ```
 
-Note that the module name is its namespace, so in this example the type `HashMap` was qualified with `Std`, the package where it is defined.
-It is possible to open a module, so that all its data structures and functions are available without this namespace qualification:
+In this example, the type `HashMap` is qualified with `Std`, the namespace where it is defined.
+All resources in the standard library are in the same namespace, `Std`.
+
+It is also possible to open a module so that all its data structures and functions are available without this namespace qualification:
 
 ```lean
 import Std