diff --git a/Manual/BuildTools/Lake.lean b/Manual/BuildTools/Lake.lean
index 9cfa7cc5a..284e42b5f 100644
--- a/Manual/BuildTools/Lake.lean
+++ b/Manual/BuildTools/Lake.lean
@@ -155,7 +155,7 @@ A build consists of the following steps:
   During a build, Lake records which source files or other artifacts were used to produce each artifact, saving a hash of each input; these {deftech}_traces_ are saved in the {tech}[build directory].{margin}[More specifically, each artifact's trace file contains a Merkle tree hash mixture of its inputs' hashes.]
   If the inputs are all unmodified, then the corresponding artifact is not rebuilt.
   Trace files additionally record the {tech}[log] from each build task; these outputs are replayed as if the artifact had been built anew.
-  Re-using prior build products when possible is called an {deftech}_incremental build_.
+  Reusing prior build products when possible is called an {deftech}_incremental build_.
 
 : Building artifacts
 
diff --git a/Manual/BuildTools/Lake/CLI.lean b/Manual/BuildTools/Lake/CLI.lean
index 458ed01a8..7eb959fd0 100644
--- a/Manual/BuildTools/Lake/CLI.lean
+++ b/Manual/BuildTools/Lake/CLI.lean
@@ -230,7 +230,7 @@ Lake itself can be configured with the following environment variables:
 
 *
   * {envVar +def}`LAKE_CACHE_ARTIFACT_ENDPOINT`
-  * The base URL for for the {ref "lake-cache-remote"}[remote artifact cache] used for artifact uploads.
+  * The base URL for the {ref "lake-cache-remote"}[remote artifact cache] used for artifact uploads.
     If set, then {envVar}`LAKE_CACHE_REVISION_ENDPOINT` must also be set.
     If neither of these are set, Lake will use Reservoir instead.
 
@@ -1160,7 +1160,7 @@ If {lakeOpt}`--scope` is set, Lake will use the specified scope verbatim.
 
 Artifacts are uploaded to the artifact endpoint with a file name derived from their Lake content hash (and prefixed by the repository or scope).
 The mappings file is uploaded to the revision endpoint with a file name derived from the package's current Git revision (and prefixed by the full scope).
-As such, the command will warn if the the work tree currently has changes.
+As such, the command will warn if the work tree currently has changes.
 ::::
 
 
diff --git a/Manual/BuildTools/Lake/Config.lean b/Manual/BuildTools/Lake/Config.lean
index 339a9b4bd..94bd97985 100644
--- a/Manual/BuildTools/Lake/Config.lean
+++ b/Manual/BuildTools/Lake/Config.lean
@@ -106,7 +106,7 @@ Libraries, executables, and other {tech}[targets] within a package can further a
 :::tomlFieldCategory "Testing and Linting" testDriver testDriverArgs lintDriver lintDriverArgs
 
 The CLI commands {lake}`test` and {lake}`lint` use definitions configured by the {tech}[workspace]'s {tech}[root package] to perform testing and linting.
-The code that is run to perform tests and lits are referred to as the test or lint driver.
+The code that is run to perform tests and linting is referred to as the test or lint driver.
 In Lean configuration files, these can be specified by applying the `@[test_driver]` or `@[lint_driver]` attributes to a {tech}[Lake script] or an executable or library target.
 In both Lean and TOML configuration files, they can also be configured by setting these options.
 A target or script `TGT` from a dependency `PKG` can be specified as a test or lint driver using the string `"PKG/TGT"`
diff --git a/Manual/Meta/LakeCmd.lean b/Manual/Meta/LakeCmd.lean
index 364e2a566..1e25cc54a 100644
--- a/Manual/Meta/LakeCmd.lean
+++ b/Manual/Meta/LakeCmd.lean
@@ -246,7 +246,7 @@ def lakeCommand.descr : BlockDescr where
 
   traverse id info _ := do
     let Json.arr #[Json.str name, aliases, _] := info
-      | do logError s!"Failed to deserialize data while traversing a Lake command, expected 3-element array startign with string but got {info}"; pure none
+      | do logError s!"Failed to deserialize data while traversing a Lake command, expected 3-element array starting with string but got {info}"; pure none
     let aliases : List String ←
       match fromJson? (α := List String) aliases with
       | .ok v => pure v
diff --git a/Manual/Meta/LakeToml/Test.lean b/Manual/Meta/LakeToml/Test.lean
index 051366da8..fc052acbe 100644
--- a/Manual/Meta/LakeToml/Test.lean
+++ b/Manual/Meta/LakeToml/Test.lean
@@ -12,7 +12,7 @@ namespace Manual.Toml
 open Std (Format)
 open Lean Elab
 
-/-- Types that can be used in in-manual tests for TOML decoding -/
+/-- Types that can be used in tests embedded in the manual for TOML decoding -/
 class Test (α : Sort u) where
   toString : α → Format