diff --git a/Manual/BasicTypes/Char.lean b/Manual/BasicTypes/Char.lean
index c114cf59a..1bbe8ea88 100644
--- a/Manual/BasicTypes/Char.lean
+++ b/Manual/BasicTypes/Char.lean
@@ -53,7 +53,7 @@ tag := "char-syntax"
 %%%
 
 Character literals consist of a single character or an escape sequence enclosed in single quotes (`'`, Unicode `'APOSTROPHE' (U+0027)`).
-Between these single quotes, the character literal may contain character other that `'`, including newlines, which are included literally (with the caveat that all newlines in a Lean source file are interpreted as `'\n'`, regardless of file encoding and platform).
+Between these single quotes, the character literal may contain any character other than `'`, including newlines, which are included literally (with the caveat that all newlines in a Lean source file are interpreted as `'\n'`, regardless of file encoding and platform).
 Special characters may be escaped with a backslash, so `'\''` is a character literal that contains a single quote.
 The following forms of escape sequences are accepted:
 
diff --git a/Manual/BasicTypes/Float.lean b/Manual/BasicTypes/Float.lean
index ba92da562..956894b3a 100644
--- a/Manual/BasicTypes/Float.lean
+++ b/Manual/BasicTypes/Float.lean
@@ -23,7 +23,7 @@ set_option pp.rawOnError true
 tag := "Float"
 %%%
 
-Floating-point numbers are a an approximation of the real numbers that are efficiently implemented in computer hardware.
+Floating-point numbers are an approximation of the real numbers that are efficiently implemented in computer hardware.
 Computations that use floating-point numbers are very efficient; however, the nature of the way that they approximate the real numbers is complex, with many corner cases.
 The IEEE 754 standard, which defines the floating-point format that is used on modern computers, allows hardware designers to make certain choices, and real systems differ in these small details.
 For example, there are many distinct bit representations of `NaN`, the indicator that a result is undefined, and some platforms differ with respect to _which_ `NaN` is returned from adding two `NaN`s.
diff --git a/Manual/BasicTypes/Int.lean b/Manual/BasicTypes/Int.lean
index 11c4345f9..35fe9bc3b 100644
--- a/Manual/BasicTypes/Int.lean
+++ b/Manual/BasicTypes/Int.lean
@@ -183,7 +183,7 @@ All evaluate to 0.
 
 ## Bitwise Operators
 
-Bitwise operators on {name}`Int` can be understood as bitwise operators on an infinite stream of bits that are the twos-complement representation of integers.
+Bitwise operators on {name}`Int` can be understood as bitwise operators on an infinite stream of bits that are the two's-complement representation of integers.
 
 {docstring Int.not}
 
diff --git a/Manual/BasicTypes/UInt.lean b/Manual/BasicTypes/UInt.lean
index e535442ef..91e4ca4c9 100644
--- a/Manual/BasicTypes/UInt.lean
+++ b/Manual/BasicTypes/UInt.lean
@@ -29,7 +29,7 @@ In compiled code, they are represented efficiently: the compiler has special sup
 Fixed-width integers may be unsigned or signed.
 Furthermore, they are available in five sizes: 8, 16, 32, and 64 bits, along with the current architecture's word size.
 In their logical models, the unsigned integers are structures that wrap a {name}`BitVec` of the appropriate width.
-Signed integers wrap the corresponding unsigned integers, and use a twos-complement representation.
+Signed integers wrap the corresponding unsigned integers, and use a two's-complement representation.
 
 ## Unsigned
 
@@ -108,7 +108,7 @@ theorem Permissions.decode_encode (p : Permissions) : p = .decode (p.encode) :=
 :::
 
 Literals that overflow their types' precision are interpreted modulus the precision.
-Signed types, are interpreted according to the underlying twos-complement representation.
+Signed types, are interpreted according to the underlying two's-complement representation.
 
 :::example "Overflowing Fixed-Width Literals"
 The following statements are all true:
diff --git a/Manual/BuildTools/Lake/CLI.lean b/Manual/BuildTools/Lake/CLI.lean
index 458ed01a8..26b263c3d 100644
--- a/Manual/BuildTools/Lake/CLI.lean
+++ b/Manual/BuildTools/Lake/CLI.lean
@@ -956,13 +956,13 @@ They are likely change in future versions of Lake based on user feedback.
 Packages that use Reservoir cloud build archives should enable the {tomlField Lake.PackageConfig}`platformIndependent` setting.
 
 ```lakeHelp "pack"
-Pack build artifacts into a archive for distribution
+Pack build artifacts into an archive for distribution
 
 USAGE:
   lake pack [<file.tgz>]
 
 Packs the root package's `buildDir` into a gzip tar archive using `tar`.
-If a path for the archive is not specified, creates a archive in the package's
+If a path for the archive is not specified, creates an archive in the package's
 Lake directory (`.lake`) named according to its `buildArchive` setting.
 
 Does NOT build any artifacts. It just packs the existing ones.
@@ -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/Classes/DerivingHandlers.lean b/Manual/Classes/DerivingHandlers.lean
index cdccbf7ea..4c4a42509 100644
--- a/Manual/Classes/DerivingHandlers.lean
+++ b/Manual/Classes/DerivingHandlers.lean
@@ -51,7 +51,7 @@ private def checkDerivable (expected : Array Name) : CommandElabM Unit := do
     unless missing.isEmpty do
       logError
         m!"These classes were expected but not present. Check whether the text needs updating, then \
-           then remove them from the call."
+           remove them from the call."
 
 end
 
diff --git a/Manual/Grind/Algebra.lean b/Manual/Grind/Algebra.lean
index 63fc6714e..2ef6a6dcb 100644
--- a/Manual/Grind/Algebra.lean
+++ b/Manual/Grind/Algebra.lean
@@ -216,7 +216,7 @@ tag := "NoNatZeroDivisors"
 
 The class `NoNatZeroDivisors` is used to control coefficient growth.
 For example, the polynomial `2 * x * y + 4 * z = 0` is simplified to `x * y + 2 * z = 0`.
-It also used when processing disequalities.
+It is also used when processing disequalities.
 
 :::example "Using `NoNatZeroDivisors`"
 ```lean -show
diff --git a/Manual/Grind/CaseAnalysis.lean b/Manual/Grind/CaseAnalysis.lean
index 91ab1b555..b08e25d84 100644
--- a/Manual/Grind/CaseAnalysis.lean
+++ b/Manual/Grind/CaseAnalysis.lean
@@ -23,7 +23,7 @@ tag := "grind-split"
 %%%
 
 In addition to congruence closure and constraint propagation, {tactic}`grind` performs case analysis.
-During case analysis, {tactic}`grind` considers each possible way that a term could have been built, or each possbile value of a particular term, in a manner similar to the {tactic}`cases` and {tactic}`split` tactics.
+During case analysis, {tactic}`grind` considers each possible way that a term could have been built, or each possible value of a particular term, in a manner similar to the {tactic}`cases` and {tactic}`split` tactics.
 This case analysis is not exhaustive: {tactic}`grind` only recursively splits cases up to a configured depth limit, and configuration options and annotations control which terms are candidates for splitting.
 
 
diff --git a/Manual/Grind/EMatching.lean b/Manual/Grind/EMatching.lean
index abd176ae9..9cbb7a493 100644
--- a/Manual/Grind/EMatching.lean
+++ b/Manual/Grind/EMatching.lean
@@ -748,7 +748,7 @@ h₄: [p (#2 + 2), q #1]
 axiom p : Nat → Nat
 axiom q : Nat → Nat
 ```
-In this example, pattern generation fails because the theorem's conclusion doesn't mention the the argument `y`.
+In this example, pattern generation fails because the theorem's conclusion doesn't mention the argument `y`.
 ```lean (name := h5) +error
 @[grind? ←] theorem h₅ (w : p x = q y) : p (x + 2) = 7 := sorry
 ```
diff --git a/Manual/Grind/ExtendedExamples/IfElseNorm.lean b/Manual/Grind/ExtendedExamples/IfElseNorm.lean
index 910505770..1fe513527 100644
--- a/Manual/Grind/ExtendedExamples/IfElseNorm.lean
+++ b/Manual/Grind/ExtendedExamples/IfElseNorm.lean
@@ -418,7 +418,7 @@ theorem normalize_spec
   fun_induction normalize with grind
 ```
 
-(The fact that we can do this relies on the fact that all the lemmas for both {name}`HashMap` and for {name}`TreeMap` that {tactic}`grind` needs have already be annotated in the standard library.)
+(The fact that we can do this relies on the fact that all the lemmas for both {name}`HashMap` and for {name}`TreeMap` that {tactic}`grind` needs have already been annotated in the standard library.)
 
 If you'd like to play around with this code,
 you can find the whole file [here](https://github.com/leanprover/lean4/blob/master/tests/lean/run/grind_ite.lean),
diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
index 2a39b9c12..d2acd6dc0 100644
--- a/Manual/Language/InductiveTypes.lean
+++ b/Manual/Language/InductiveTypes.lean
@@ -160,7 +160,7 @@ Solo.solo : Solo
 inductive Yes : Prop where
   | intro
 ```
-Unlike {lean}`One`, the new inductive type {lean}`Yes` is specified to be in the {lean}`Prop` universe.
+Unlike {lean}`Solo`, the new inductive type {lean}`Yes` is specified to be in the {lean}`Prop` universe.
 ```lean (name := YesTy)
 #check Yes
 ```
diff --git a/Manual/Language/InductiveTypes/LogicalModel.lean b/Manual/Language/InductiveTypes/LogicalModel.lean
index a7ffa9f52..110f258d3 100644
--- a/Manual/Language/InductiveTypes/LogicalModel.lean
+++ b/Manual/Language/InductiveTypes/LogicalModel.lean
@@ -368,7 +368,7 @@ tag := "recursor-elaboration-helpers"
 %%%
 
 In addition to the type constructor, constructors, and recursors that Lean's core type theory prescribes for inductive types, Lean constructs a number of useful helpers.
-First, the equation compiler (which translates recursive functions with pattern matching in to applications of recursors) makes use of these additional constructs:
+First, the equation compiler (which translates recursive functions with pattern matching into applications of recursors) makes use of these additional constructs:
  * `recOn` is a version of the recursor in which the major premise is prior to the minor premise for each constructor.
  * `casesOn` is a version of the recursor in which the major premise is prior to the minor premise for each constructor, and recursive arguments do not yield induction hypotheses. It expresses case analysis rather than primitive recursion.
  * `below` computes a type that, for some motive, expresses that _all_ inhabitants of the inductive type that are subtrees of the major premise satisfy the motive. It transforms a motive for induction or primitive recursion into a motive for strong recursion or strong induction.
diff --git a/Manual/Monads/API.lean b/Manual/Monads/API.lean
index 9071ae137..83938c139 100644
--- a/Manual/Monads/API.lean
+++ b/Manual/Monads/API.lean
@@ -22,7 +22,7 @@ set_option linter.unusedVariables false
 
 #doc (Manual) "API Reference" =>
 
-In addition to the general functions described here, there are some functions that are conventionally defined as part of the API of in the namespace of each collection type:
+In addition to the general functions described here, there are some functions that are conventionally defined as part of the API in the namespace of each collection type:
  * `mapM` maps a monadic function.
  * `forM` maps a monadic function, throwing away the result.
  * `filterM` filters using a monadic predicate, returning the values that satisfy it.
@@ -100,7 +100,7 @@ The {name}`discard` function is especially useful when using an action that retu
 # Re-Ordered Operations
 
 Sometimes, it can be convenient to partially apply a function to its second argument.
-These functions reverse the order of arguments, making it this easier.
+These functions reverse the order of arguments, making this easier.
 
 {docstring Functor.mapRev}
 
diff --git a/Manual/Namespaces.lean b/Manual/Namespaces.lean
index 053499324..2e9ebdf4f 100644
--- a/Manual/Namespaces.lean
+++ b/Manual/Namespaces.lean
@@ -203,7 +203,7 @@ Without an identifier, {keywordOf Lean.Parser.Command.end}`end` closes the most
 end
 ```
 
-With an identifier, it closes the most recently opened section section or namespace.
+With an identifier, it closes the most recently opened section or namespace.
 If it is a section, the identifier must be a suffix of the concatenated names of the sections opened since the most recent {keywordOf Lean.Parser.Command.namespace}`namespace` command.
 If it is a namespace, then the identifier must be a suffix of the current namespace's extensions since the most recent {keywordOf Lean.Parser.Command.section}`section` that is still open; afterwards, the current namespace will have had this suffix removed.
 ```grammar
diff --git a/Manual/Releases/v4_10_0.lean b/Manual/Releases/v4_10_0.lean
index 58063fa42..cc962d5d0 100644
--- a/Manual/Releases/v4_10_0.lean
+++ b/Manual/Releases/v4_10_0.lean
@@ -166,7 +166,7 @@ file := "v4.10.0"
   * [#4499](https://github.com/leanprover/lean4/pull/4499) introduces `Std`, a library situated between `Init` and `Lean`, providing functionality not in the prelude both to Lean's implementation and to external users.
 * **Other fixes or improvements**
   * [#3056](https://github.com/leanprover/lean4/pull/3056) standardizes on using `(· == a)` over `(a == ·)`.
-  * [#4502](https://github.com/leanprover/lean4/pull/4502) fixes errors reported by running the library through the the Batteries linters.
+  * [#4502](https://github.com/leanprover/lean4/pull/4502) fixes errors reported by running the library through the Batteries linters.
 
 ### Lean internals
 
diff --git a/Manual/Releases/v4_15_0.lean b/Manual/Releases/v4_15_0.lean
index 7736ec447..7f1dc77a0 100644
--- a/Manual/Releases/v4_15_0.lean
+++ b/Manual/Releases/v4_15_0.lean
@@ -489,7 +489,7 @@ make proving inequalities about `USize.size` easier.
 
 - [#6205](https://github.com/leanprover/lean4/pull/6205) upstreams some UInt theorems from Batteries and adds more
 `toNat`-related theorems. It also adds the missing `UInt8` and `UInt16`
-to/from `USize` conversions so that the the interface is uniform across
+to/from `USize` conversions so that the interface is uniform across
 the UInt types.
 
 - [#6207](https://github.com/leanprover/lean4/pull/6207) ensures the `Fin.foldl` and `Fin.foldr` are semireducible.
diff --git a/Manual/Releases/v4_16_0.lean b/Manual/Releases/v4_16_0.lean
index 489ac8235..77cef5f27 100644
--- a/Manual/Releases/v4_16_0.lean
+++ b/Manual/Releases/v4_16_0.lean
@@ -548,7 +548,7 @@ none) using the necessary flags.
 * [#6289](https://github.com/leanprover/lean4/pull/6289) adapts Lake modules to use `prelude` and includes them in the
 `check-prelude` CI.
 
-* [#6291](https://github.com/leanprover/lean4/pull/6291) ensures the the log error position is properly preserved when
+* [#6291](https://github.com/leanprover/lean4/pull/6291) ensures the log error position is properly preserved when
 prepending stray log entries to the job log. It also adds comparison
 support for `Log.Pos`.
 
diff --git a/Manual/Releases/v4_17_0.lean b/Manual/Releases/v4_17_0.lean
index f34b40084..1343e4374 100644
--- a/Manual/Releases/v4_17_0.lean
+++ b/Manual/Releases/v4_17_0.lean
@@ -461,7 +461,7 @@ theorem:
   ```lean
   theorem inv_eq {a b : α} (w : a * b = 1) : inv a = b
   ```
-  and we want to instantiate the theorem whenever we are tying to prove
+  and we want to instantiate the theorem whenever we are trying to prove
 `inv t = s` for some terms `t` and `s`
 The attribute `[grind ←]` is not applicable in this case because, by
 default, `=` is not eligible for E-matching. The new attribute `[grind
diff --git a/Manual/Releases/v4_20_0.lean b/Manual/Releases/v4_20_0.lean
index 7526ce8fa..1a312e836 100644
--- a/Manual/Releases/v4_20_0.lean
+++ b/Manual/Releases/v4_20_0.lean
@@ -1095,7 +1095,7 @@ Other notable library developments in this release include:
   no longer incorporate their module's source trace.
 
 * [#7909](https://github.com/leanprover/lean4/pull/7909) adds Lake support for building modules given their source file
-  path. This is made use of in both the CLI and the sever.
+  path. This is made use of in both the CLI and the server.
 
 * [#7963](https://github.com/leanprover/lean4/pull/7963) adds helper functions to convert between `Lake.EStateT` and
   `EStateM`.
diff --git a/Manual/Releases/v4_21_0.lean b/Manual/Releases/v4_21_0.lean
index 89091f2f4..40daa666d 100644
--- a/Manual/Releases/v4_21_0.lean
+++ b/Manual/Releases/v4_21_0.lean
@@ -304,7 +304,7 @@ _Other Highlights_
 * [#8301](https://github.com/leanprover/lean4/pull/8301) unfolds functions in the unfolding induction principle properly
   when they use `bif` (a.k.a. `Bool.cond`).
 
-* [#8302](https://github.com/leanprover/lean4/pull/8302) lets `cases` fail gracefully when the motive has an complex
+* [#8302](https://github.com/leanprover/lean4/pull/8302) lets `cases` fail gracefully when the motive has a complex
   argument whose type is dependent type on the targets. While the
   `induction` tactic can handle this well, `cases` does not. This change
   at least gracefully degrades to not instantiating that motive parameter.
@@ -600,7 +600,7 @@ _Other Highlights_
   `BitVec.one_eq_zero_iff`
 
 * [#8206](https://github.com/leanprover/lean4/pull/8206) shows that negating a bitvector created from a natural number
-  equals creating a bitvector from the the negative of that number (as an
+  equals creating a bitvector from the negative of that number (as an
   integer).
 
 * [#8216](https://github.com/leanprover/lean4/pull/8216) completes adding `@[grind]` annotations for `Option` lemmas, and
@@ -770,7 +770,7 @@ _Other Highlights_
 
 * [#8620](https://github.com/leanprover/lean4/pull/8620) removes the `NatCast (Fin n)` global instance (both the direct
   instance, and the indirect one via `Lean.Grind.Semiring`), as that
-  instance causes causes `x < n` (for `x : Fin k`, `n : Nat`) to be
+  instance causes `x < n` (for `x : Fin k`, `n : Nat`) to be
   elaborated as `x < ↑n` rather than `↑x < n`, which is undesirable. Note
   however that in Mathlib this happens anyway!
 
@@ -928,7 +928,7 @@ _Other Highlights_
   name would not be caught and cause loading to fail.
 
 * [#8529](https://github.com/leanprover/lean4/pull/8529) changes `lake lean` and `lake setup-file` to precompile the
-  imports of non-workspace files using the the import's whole library.
+  imports of non-workspace files using the import's whole library.
   This ensures that additional link objects are linked and available
   during elaboration.
 
diff --git a/Manual/Releases/v4_22_0.lean b/Manual/Releases/v4_22_0.lean
index f9f223fdf..78c18300c 100644
--- a/Manual/Releases/v4_22_0.lean
+++ b/Manual/Releases/v4_22_0.lean
@@ -403,7 +403,7 @@ When false, the warning is not logged.
   linarith modules in grind.
 
 * [#8694](https://github.com/leanprover/lean4/pull/8694) implements special support for `One.one` in linarith when the
-  structure is a ordered ring. It also fixes bugs during initialization.
+  structure is an ordered ring. It also fixes bugs during initialization.
 
 * [#8697](https://github.com/leanprover/lean4/pull/8697) implements support for inequalities in the `grind` linear
   arithmetic procedure and simplifies its design. Some examples that can
@@ -1068,7 +1068,7 @@ When false, the warning is not logged.
 
 * [#8620](https://github.com/leanprover/lean4/pull/8620) removes the `NatCast (Fin n)` global instance (both the direct
   instance, and the indirect one via `Lean.Grind.Semiring`), as that
-  instance causes causes `x < n` (for `x : Fin k`, `n : Nat`) to be
+  instance causes `x < n` (for `x : Fin k`, `n : Nat`) to be
   elaborated as `x < ↑n` rather than `↑x < n`, which is undesirable. Note
   however that in Mathlib this happens anyway!
 
diff --git a/Manual/Releases/v4_23_0.lean b/Manual/Releases/v4_23_0.lean
index d86f69eae..5bae342eb 100644
--- a/Manual/Releases/v4_23_0.lean
+++ b/Manual/Releases/v4_23_0.lean
@@ -586,7 +586,7 @@ In terms of user experience, noteworthy new features are:
 
 * [#9670](https://github.com/leanprover/lean4/pull/9670) add constructors `.intCast k` and `.natCast k` to
   `CommRing.Expr`. We need them because terms such as `Nat.cast (R := α)
-  1` and `(1 : α)` are not definitionally equal. This is pervaise in
+  1` and `(1 : α)` are not definitionally equal. This is pervasive in
   Mathlib for the numerals `0` and `1`.
 
 * [#9671](https://github.com/leanprover/lean4/pull/9671) fixes support for `SMul.smul` in `grind ring`. `SMul.smul`
diff --git a/Manual/Releases/v4_27_0.lean b/Manual/Releases/v4_27_0.lean
index 885f575d5..ac1741b92 100644
--- a/Manual/Releases/v4_27_0.lean
+++ b/Manual/Releases/v4_27_0.lean
@@ -35,7 +35,7 @@ For this release, 372 changes landed. In addition to the 118 feature additions a
   `MatcherInfo`, and using that during matcher calculation.
 
 * [#11200](https://github.com/leanprover/lean4/pull/11200) changes how sparse case expressions represent the
-  none-of-the-above information. Instead of of many `x.ctorIdx ≠ i`
+  none-of-the-above information. Instead of many `x.ctorIdx ≠ i`
   hypotheses, it introduces a single `Nat.hasNotBit mask x.ctorIdx`
   hypothesis which compresses that information into a bitmask. This avoids
   a quadratic overhead during splitter generation, where all n assumptions
@@ -155,7 +155,7 @@ For this release, 372 changes landed. In addition to the 118 feature additions a
 * [#11453](https://github.com/leanprover/lean4/pull/11453) fixes undefined behavior where `delete` (instead of `delete[]`)
   is called on an object allocated with `new[]`.
 
-* [#11456](https://github.com/leanprover/lean4/pull/11456) refines several error error messages, mostly involving invalid
+* [#11456](https://github.com/leanprover/lean4/pull/11456) refines several error messages, mostly involving invalid
   use of field notation, generalized field notation, and numeric
   projection. Provides a new error explanation for field notation.
 
@@ -182,7 +182,7 @@ For this release, 372 changes landed. In addition to the 118 feature additions a
   those using `aesop`) being affected by the current recursion depth or
   heartbeat limit.
 
-* [#11492](https://github.com/leanprover/lean4/pull/11492) uses the the helper functions withImplicitBinderInfos and
+* [#11492](https://github.com/leanprover/lean4/pull/11492) uses the helper functions withImplicitBinderInfos and
   mkArrowN in more places.
 
 * [#11493](https://github.com/leanprover/lean4/pull/11493) makes `Match.MatchEqs` a leaf module, to be less restricted in
diff --git a/Manual/Releases/v4_8_0.lean b/Manual/Releases/v4_8_0.lean
index 910384530..ecba9579f 100644
--- a/Manual/Releases/v4_8_0.lean
+++ b/Manual/Releases/v4_8_0.lean
@@ -379,7 +379,7 @@ file := "v4.8.0"
 
 * **TOML Lake configurations**. [#3298](https://github.com/leanprover/lean4/pull/3298), [#4104](https://github.com/leanprover/lean4/pull/4104).
 
-  Lake packages can now use TOML as a alternative configuration file format instead of Lean. If the default `lakefile.lean` is missing, Lake will also look for a `lakefile.toml`. The TOML version of the configuration supports a restricted set of the Lake configuration options, only including those which can easily mapped to a TOML data structure. The TOML syntax itself fully compiles with the TOML v1.0.0 specification.
+  Lake packages can now use TOML as an alternative configuration file format instead of Lean. If the default `lakefile.lean` is missing, Lake will also look for a `lakefile.toml`. The TOML version of the configuration supports a restricted set of the Lake configuration options, only including those which can easily mapped to a TOML data structure. The TOML syntax itself fully compiles with the TOML v1.0.0 specification.
 
   As part of the introduction of this new feature, we have been helping maintainers of some major packages within the ecosystem switch to this format. For example, the following is Aesop's new `lakefile.toml`:
 
diff --git a/Manual/Tactics/Reference.lean b/Manual/Tactics/Reference.lean
index 8fc6eb160..07516bc9f 100644
--- a/Manual/Tactics/Reference.lean
+++ b/Manual/Tactics/Reference.lean
@@ -225,7 +225,7 @@ tag := "tactic-ref-goals"
 tag := "tactic-ref-casts"
 %%%
 
-The tactics in this section make it easier avoid getting stuck on {deftech}_casts_, which are functions that coerce data from one type to another, such as converting a natural number to the corresponding integer.
+The tactics in this section make it easier to avoid getting stuck on {deftech}_casts_, which are functions that coerce data from one type to another, such as converting a natural number to the corresponding integer.
 They are described in more detail by {citet castPaper}[].
 
 :::tactic Lean.Parser.Tactic.tacticNorm_cast__
@@ -465,7 +465,7 @@ tag := "tactic-ref-search"
 %%%
 
 The library search tactics are intended for interactive use.
-When run, they search the Lean library for lemmas or rewrite rules that could be applicable in the current situation, and suggests a new tactic.
+When run, they search the Lean library for lemmas or rewrite rules that could be applicable in the current situation, and suggest a new tactic.
 These tactics should not be left in a proof; rather, their suggestions should be incorporated.
 
 :::tactic "exact?"
diff --git a/Manual/Terms.lean b/Manual/Terms.lean
index 090545f91..d0b1073e4 100644
--- a/Manual/Terms.lean
+++ b/Manual/Terms.lean
@@ -113,7 +113,7 @@ The innermost local binding of a name takes precedence over others:
 
 ::::keepEnv
 :::example "Longer Prefixes of Current Namespace Take Precedence"
-The  namespaces `A`, `B`, and `C` are nested.
+The namespaces `A`, `B`, and `C` are nested.
 Both `A` and `C` contain a definition of `x`.
 ```lean (name := NS)
 namespace A
@@ -674,7 +674,7 @@ fun x => (fun x y => sum3 x y 8) x 1 : Nat → Nat
 ```
 
 Parameter names are taken from the function's _type_, and the names used for function parameters don't need to match the names used in the type.
-This means that local bindings that conflict with a parameter's name don't prevent the use of named parameters, because Lean avoids this conflicts by renaming the function's parameter while leaving the name intact in the type.
+This means that local bindings that conflict with a parameter's name don't prevent the use of named parameters, because Lean avoids these conflicts by renaming the function's parameter while leaving the name intact in the type.
 ```lean (name := sum15)
 #check let x := 15; sum3 (z := x)
 ```
@@ -1010,7 +1010,7 @@ Scientific numbers are overloaded via the {name}`OfScientific` type class.
 
 {docstring OfScientific}
 
-There are an {lean}`OfScientific` instances for {name}`Float` and {name}`Float32`, but no separate floating-point literals.
+There are {lean}`OfScientific` instances for {name}`Float` and {name}`Float32`, but no separate floating-point literals.
 
 ## Strings