diff --git a/doc/dev/bootstrap.md b/doc/dev/bootstrap.md
index 43ad0b025e..8e889f4726 100644
--- a/doc/dev/bootstrap.md
+++ b/doc/dev/bootstrap.md
@@ -75,7 +75,7 @@ The github repository will automatically update stage0 on `master` once
 
 NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
 Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.
-The same is true for further stages except that a rebuild of them is retriggered on any commited change, not just to a specific directory.
+The same is true for further stages except that a rebuild of them is retriggered on any committed change, not just to a specific directory.
 Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
 
 If you have write access to the lean4 repository, you can also manually
diff --git a/src/Init/Data/Order/PackageFactories.lean b/src/Init/Data/Order/PackageFactories.lean
index 548e20cdc8..f8d0beee98 100644
--- a/src/Init/Data/Order/PackageFactories.lean
+++ b/src/Init/Data/Order/PackageFactories.lean
@@ -734,7 +734,7 @@ public structure Packages.LinearOrderOfOrdArgs (α : Type u) extends
     | exact fun a b => Std.min_eq_if_isLE_compare (a := a) (b := b)
     | fail "Failed to automatically prove that `min` is left-leaning. \
             Please ensure that a `LawfulOrderLeftLeaningMin` instance can be synthesized or \
-            manuelly provide the field `min_eq`."
+            manually provide the field `min_eq`."
   max_eq :
       let := ord; let := le; let := max; have := lawfulOrderOrd
       ∀ a b : α, Max.max a b = if (compare a b).isGE then a else b := by
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 997dfa1404..8ca34738a4 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -146,7 +146,7 @@ variable (sep : String) (escape : Bool) in
 Uses the separator `sep` (usually `"."`) to combine the components of the `Name` into a string.
 See the documentation for `Name.toStringWithToken` for an explanation of `escape` and `isToken`.
 -/
-@[specialize isToken] -- explicit annotation because isToken is overriden in recursive call
+@[specialize isToken] -- explicit annotation because isToken is overridden in recursive call
 def toStringWithSep (n : Name) (isToken : String → Bool := fun _ => false) : String :=
   match n with
   | anonymous       => "[anonymous]"
diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean
index 1cd6546b22..bdb40d8bd9 100644
--- a/src/Lean/Compiler/IR/CompilerM.lean
+++ b/src/Lean/Compiler/IR/CompilerM.lean
@@ -158,7 +158,7 @@ def findEnvDecl (env : Environment) (declName : Name) : Option Decl :=
   match env.getModuleIdxFor? declName with
   | some modIdx =>
     -- `meta import/import all` and server `#eval`
-    -- This case is important even for codegen because it needs to see IR via `import all` (beause
+    -- This case is important even for codegen because it needs to see IR via `import all` (because
     -- it can also see the LCNF)
     findAtSorted? (declMapExt.getModuleIREntries env modIdx) declName <|>
     -- (closure of) `meta def`; will report `.extern`s for other `def`s so needs to come second
diff --git a/src/Lean/Compiler/MetaAttr.lean b/src/Lean/Compiler/MetaAttr.lean
index 8a29a41a82..81b75cd49b 100644
--- a/src/Lean/Compiler/MetaAttr.lean
+++ b/src/Lean/Compiler/MetaAttr.lean
@@ -39,7 +39,7 @@ def getIRPhases (env : Environment) (declName : Name) : IRPhases := Id.run do
       .comptime
     else
       env.header.modules[idx.toNat]?.map (·.irPhases) |>.get!
-  -- Allow `meta`->non-`meta` acesses in the same module
+  -- Allow `meta`->non-`meta` accesses in the same module
   | none => if isMeta env declName then .comptime else .all
 
 end Lean
diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean
index b17e485049..9091c6f39e 100644
--- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean
+++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean
@@ -177,7 +177,7 @@ def deriveInduction (name : Name) (isMutual : Bool) : MetaM Unit := do
         let motives ← forallTelescope eTyp fun args _ => do
           let motives ← unfoldPredRelMutual eqnInfo (←inferType args[1]!) (reduceConclusion := true)
           motives.mapM (fun x => mkForallFVars #[args[0]!] x)
-        -- For each predicate in the mutual group we generate an approprate candidate predicate
+        -- For each predicate in the mutual group we generate an appropriate candidate predicate
         let predicates := (numberNames infos.size "pred").zip <| ← PProdN.unpack α infos.size
         -- Then we make the induction principle more readable, by currying the hypotheses and projecting the conclusion
         withLocalDeclsDND predicates fun predVars => do
diff --git a/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean b/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean
index 6ee9f964a7..be3ba5de8c 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean
@@ -40,7 +40,7 @@ Preprocesses the expressions to improve the effectiveness of `elimRecursion`.
     | i+1 => (f x) i
   ```
 
-* Unfold auxillary definitions abstracting over the function call
+* Unfold auxiliary definitions abstracting over the function call
   (typically abstracted) proofs.
 
 -/
diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index ce8a31b7d9..c9357bec96 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -810,9 +810,9 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
 
   -- For every function, the measures we want to use
   -- (One for each non-forbiddend arg)
-  let basicMeassures₁ ← simpleMeasures preDefs fixedParamPerms userVarNamess
-  let basicMeassures₂ ← complexMeasures preDefs fixedParamPerms userVarNamess recCalls
-  let basicMeasures := Array.zipWith (· ++ ·) basicMeassures₁ basicMeassures₂
+  let basicMeasures₁ ← simpleMeasures preDefs fixedParamPerms userVarNamess
+  let basicMeasures₂ ← complexMeasures preDefs fixedParamPerms userVarNamess recCalls
+  let basicMeasures := Array.zipWith (· ++ ·) basicMeasures₁ basicMeasures₂
 
   -- The list of measures, including the measures that order functions.
   -- The function ordering measures come last
diff --git a/src/Lean/Elab/PreDefinition/WF/Unfold.lean b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
index a4e90f475e..224315975b 100644
--- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
@@ -182,7 +182,7 @@ builtin_simproc_decl matcherPushArg (_) := fun e => do
     mkLambdaFVars xs (.lam motiveBodyArg.bindingName! motiveBodyArg.bindingDomain! motiveBodyArg.bindingBody!.bindingDomain! .default)
 
   let argPusher ← mkMatchArgPusher matcherApp.matcherName matcherApp.toMatcherInfo
-  -- Let's infer the level paramters:
+  -- Let's infer the level parameters:
   let proof ← withTransparency .all <| mkAppOptM
     argPusher ((matcherApp.params ++ #[motive', alpha, beta, fExpr, rel] ++ matcherApp.discrs ++ matcherApp.alts).map some)
   let some (_, _, rhs) := (← inferType proof).eq? | throwError "matcherPushArg: expected equality:{indentExpr (← inferType proof)}"
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/EmbeddedConstraint.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/EmbeddedConstraint.lean
index 5a3bdf4b50..8cf367f075 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/EmbeddedConstraint.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/EmbeddedConstraint.lean
@@ -28,7 +28,7 @@ them to substitute occurrences of `x` within other hypotheses. Additionally this
 redundant top level hypotheses.
 -/
 def embeddedConstraintPass : Pass where
-  name := `embeddedConstraintSubsitution
+  name := `embeddedConstraintSubstitution
   run' goal := do
     goal.withContext do
       let hyps ← getPropHyps
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 9f1dc9557f..405a310aa2 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -179,7 +179,7 @@ private def elabDeclToUnfoldOrTheorem (config : Meta.ConfigWithKey) (id : Origin
     else
       if inv then
         throwError m!"Invalid `←` modifier: `{declName}` is a declaration name to be unfolded"
-          ++ .hint' m!"The simplifier cannot \"refold\" definitions by name. Use `rw` for this intead,
+          ++ .hint' m!"The simplifier cannot \"refold\" definitions by name. Use `rw` for this instead,
                       or use the `←` simp modifier with an equational lemma for `{declName}`."
       if kind == .dsimp then
         return .addEntries #[.toUnfold declName]
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index d6f394afaf..7f3742843c 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -2182,7 +2182,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
     serverBaseExts := (← setImportedEntries privateBase.extensions serverData)
   }
   if leakEnv then
-    /- Mark persistent a first time before `finalizePersistenExtensions`, which
+    /- Mark persistent a first time before `finalizePersistentExtensions`, which
        avoids costly MT markings when e.g. an interpreter closure (which
        contains the environment) is put in an `IO.Ref`. This can happen in e.g.
        initializers of user environment extensions and is wasteful because the
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index 54de415937..3fff800b22 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -60,7 +60,7 @@ In this module, we produce
 ```lean
 def aux := fun (y : Nat) => h (g y)
 ```
-Note that in this particular case, it is safe to lambda abstract the let-varible `y`.
+Note that in this particular case, it is safe to lambda abstract the let-variable `y`.
 This module uses the following approach to decide whether it is safe or not to lambda
 abstract a let-variable.
 1) We enable zetaDelta-expansion tracking in `MetaM`. That is, whenever we perform type checking
diff --git a/src/Lean/Meta/LetToHave.lean b/src/Lean/Meta/LetToHave.lean
index 259307a4fe..a25b3d4d21 100644
--- a/src/Lean/Meta/LetToHave.lean
+++ b/src/Lean/Meta/LetToHave.lean
@@ -45,7 +45,7 @@ Optimizations, present and future:
   however checking for `let`s is O(n), so we only try this for expressions with a small `approxDepth`.
   (We can consider precomputing this somehow.)
   - The cache is currently responsible for the check.
-  - We also do it before entering telescopes, to avoid unnecesasry fvar overhead.
+  - We also do it before entering telescopes, to avoid unnecessary fvar overhead.
 - If we are not currently inside a `let`, then we do not need to do full typechecking.
 - We try to reuse Exprs to promote subexpression sharing.
 - We might consider not transforming lets to haves if we are in a proof that is not inside a `let`.
diff --git a/src/Lean/Meta/NatTable.lean b/src/Lean/Meta/NatTable.lean
index dfee6120b1..70cb7cc9ca 100644
--- a/src/Lean/Meta/NatTable.lean
+++ b/src/Lean/Meta/NatTable.lean
@@ -12,7 +12,7 @@ import Lean.Meta.InferType
 open Lean Meta
 
 /-!
-This module provies builder for efficient `Nat → …` functions based on binary decision trees.
+This module provides builder for efficient `Nat → …` functions based on binary decision trees.
 -/
 
 /--
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 064e88add7..1eee3d1863 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -303,7 +303,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
         -- abstraction.
 
         -- To collect the IHs, we collect them in each branch, and combine
-        -- them to a type-leve match
+        -- them to a type-level match
         let ihMatcherApp' ← liftM <| matcherApp.transform
           (onParams := fun e => M.eval <| foldAndCollect oldIH newIH isRecCall e)
           (onMotive := fun xs _body => do
diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean
index c081c7fb58..bc68951ac3 100644
--- a/src/Lean/Parser/Extra.lean
+++ b/src/Lean/Parser/Extra.lean
@@ -93,7 +93,7 @@ You can use `TSyntax.getId` to extract the name from the resulting syntax object
   withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot
 
 /--
-The parser `hygieneInfo` parses no text, but creates a `hygineInfoKind` node
+The parser `hygieneInfo` parses no text, but creates a `hygieneInfoKind` node
 containing an anonymous identifier as if it were parsed at the current position.
 This identifier is modified by syntax quotations to add macro scopes like a regular identifier.
 
diff --git a/src/Lean/Server/CodeActions/UnknownIdentifier.lean b/src/Lean/Server/CodeActions/UnknownIdentifier.lean
index b0c6014cfd..c82b78548b 100644
--- a/src/Lean/Server/CodeActions/UnknownIdentifier.lean
+++ b/src/Lean/Server/CodeActions/UnknownIdentifier.lean
@@ -238,7 +238,7 @@ def handleUnknownIdentifierCodeAction
     | none => { line := 0, character := 0 }
   let importInsertionRange : Lsp.Range := ⟨importInsertionPos, importInsertionPos⟩
   let mut unknownIdentifierCodeActions := #[]
-  let mut hasUnambigiousImportCodeAction := false
+  let mut hasUnambiguousImportCodeAction := false
   let some result := response.queryResults[0]?
     | return #[]
   for query in queries, result in response.queryResults do
@@ -264,7 +264,7 @@ def handleUnknownIdentifierCodeAction
           }
         }
         if isExactMatch then
-          hasUnambigiousImportCodeAction := true
+          hasUnambiguousImportCodeAction := true
       else
         unknownIdentifierCodeActions := unknownIdentifierCodeActions.push {
           title := s!"Change to {insertion.fullName}"
@@ -274,7 +274,7 @@ def handleUnknownIdentifierCodeAction
             edits := #[insertion.edit]
           }
         }
-  if hasUnambigiousImportCodeAction then
+  if hasUnambiguousImportCodeAction then
     unknownIdentifierCodeActions := unknownIdentifierCodeActions.push <|
       importAllUnknownIdentifiersCodeAction params "quickfix"
   return unknownIdentifierCodeActions
diff --git a/src/Lean/Server/Completion/CompletionUtils.lean b/src/Lean/Server/Completion/CompletionUtils.lean
index 1056b5f0da..36af3aa6da 100644
--- a/src/Lean/Server/Completion/CompletionUtils.lean
+++ b/src/Lean/Server/Completion/CompletionUtils.lean
@@ -88,7 +88,7 @@ where
 
 /--
 Gets type names for resolving `id` in `.id x₁ ... xₙ` notation.
-The process mimics the dotted indentifier notation elaboration procedure at `Lean.Elab.App`.
+The process mimics the dotted identifier notation elaboration procedure at `Lean.Elab.App`.
 Catches and ignores all errors, so no need to run this within `try`/`catch`.
 -/
 partial def getDotIdCompletionTypeNames (type : Expr) : MetaM (Array Name) :=
diff --git a/src/Std/Do/SPred/Notation.lean b/src/Std/Do/SPred/Notation.lean
index cd76bfd40b..2f445aedd7 100644
--- a/src/Std/Do/SPred/Notation.lean
+++ b/src/Std/Do/SPred/Notation.lean
@@ -73,7 +73,7 @@ macro_rules
   | `(spred(∃ $xs:explicitBinders, $P)) => do expandExplicitBinders ``SPred.exists xs (← `(spred($P)))
   | `(⊢ₛ $P) => ``(SPred.entails ⌜True⌝ spred($P))
   | `($P ⊣⊢ₛ $Q) => ``(SPred.bientails spred($P) spred($Q))
-  -- Sadly, ∀ does not resently use expandExplicitBinders...
+  -- Sadly, ∀ does not presently use expandExplicitBinders...
   | `(spred(∀ _%$tk, $P)) => ``(SPred.forall (fun _%$tk => spred($P)))
   | `(spred(∀ _%$tk : $ty, $P)) => ``(SPred.forall (fun _%$tk : $ty => spred($P)))
   | `(spred(∀ (_%$tk $xs* : $ty), $P)) => ``(SPred.forall (fun _%$tk : $ty => spred(∀ ($xs* : $ty), $P)))
diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean
index 39738f27b9..8fa6be6c2d 100644
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@@ -32,7 +32,7 @@ structure Config where
   -/
   elimLets : Bool := true
   /--
-  If `false` (the default), then we aggresively split `if` and `match` statements and inline join
+  If `false` (the default), then we aggressively split `if` and `match` statements and inline join
   points unconditionally. For some programs this causes exponential blowup of VCs.
   Set this flag to choose a more conservative (but slightly lossy) encoding that traverses
   every join point only once and yields a formula the size of which is linear in the number of
diff --git a/src/cmake/Modules/GetGitRevisionDescription.cmake b/src/cmake/Modules/GetGitRevisionDescription.cmake
index 9f54191298..0b1ed5c570 100644
--- a/src/cmake/Modules/GetGitRevisionDescription.cmake
+++ b/src/cmake/Modules/GetGitRevisionDescription.cmake
@@ -61,7 +61,7 @@ get_filename_component(_gitdescmoddir ${CMAKE_CURRENT_LIST_FILE} PATH)
 # function returns an empty string via _git_dir_var.
 #
 # Example: Given a path C:/bla/foo/bar and assuming C:/bla/.git exists and
-# neither foo nor bar contain a file/directory .git. This wil return
+# neither foo nor bar contain a file/directory .git. This will return
 # C:/bla/.git
 #
 function(_git_find_closest_git_dir _start_dir _git_dir_var)
diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean
index 36d408ad8d..7b410f52cb 100644
--- a/src/lake/Lake/CLI/Translate/Lean.lean
+++ b/src/lake/Lake/CLI/Translate/Lean.lean
@@ -178,15 +178,15 @@ protected def Pattern.toLean? [ToLean? (PatternDescr α β)] (p : Pattern α β)
 
 instance [ToLean? (PatternDescr α β)] : ToLean? (Pattern α β) := ⟨Pattern.toLean?⟩
 
-protected partial def PattternDescr.toLean? [ToLean? β] (p : PatternDescr α β) : Option Term :=
-  have : ToLean? (PatternDescr α β) := ⟨PattternDescr.toLean?⟩
+protected partial def PatternDescr.toLean? [ToLean? β] (p : PatternDescr α β) : Option Term :=
+  have : ToLean? (PatternDescr α β) := ⟨PatternDescr.toLean?⟩
   match p with
   | .not p => quoteSingleton? `not p
   | .any p => quoteSingleton? `any p
   | .all p => quoteSingleton? `all p
   | .coe p => toLean? p
 
-instance [ToLean? β] : ToLean? (PatternDescr α β) := ⟨PattternDescr.toLean?⟩
+instance [ToLean? β] : ToLean? (PatternDescr α β) := ⟨PatternDescr.toLean?⟩
 
 protected def StrPatDescr.toLean (pat : StrPatDescr) : Term :=
   match pat with
diff --git a/src/lake/Lake/CLI/Translate/Toml.lean b/src/lake/Lake/CLI/Translate/Toml.lean
index 3a1d4a0cf1..ef7ca72218 100644
--- a/src/lake/Lake/CLI/Translate/Toml.lean
+++ b/src/lake/Lake/CLI/Translate/Toml.lean
@@ -69,7 +69,7 @@ instance : ToToml (Array LeanOption) where
 mutual
 
 partial def Pattern.toToml? [ToToml? β] (p : Pattern α β) : Option Value :=
-  have : ToToml? (PatternDescr α β) := ⟨PattternDescr.toToml?⟩
+  have : ToToml? (PatternDescr α β) := ⟨PatternDescr.toToml?⟩
   match p.name with
   | .anonymous =>
     p.descr?.bind toToml?
@@ -80,7 +80,7 @@ partial def Pattern.toToml? [ToToml? β] (p : Pattern α β) : Option Value :=
   | n =>
     toToml <| Table.empty.insert `preset n
 
-partial def PattternDescr.toToml?
+partial def PatternDescr.toToml?
   [ToToml? β] (p : PatternDescr α β) : Option Value
 :=
   have : ToToml? (Pattern α β) := ⟨Pattern.toToml?⟩
@@ -93,7 +93,7 @@ partial def PattternDescr.toToml?
 end
 
 instance [ToToml? β] : ToToml? (Pattern α β) := ⟨Pattern.toToml?⟩
-instance [ToToml? β] : ToToml? (PatternDescr α β) := ⟨PattternDescr.toToml?⟩
+instance [ToToml? β] : ToToml? (PatternDescr α β) := ⟨PatternDescr.toToml?⟩
 
 protected def StrPatDescr.toToml (p : StrPatDescr) : Value :=
   match p with
diff --git a/src/lake/Makefile b/src/lake/Makefile
index 5658162cff..1eacdbf9d3 100644
--- a/src/lake/Makefile
+++ b/src/lake/Makefile
@@ -19,7 +19,7 @@ test-tests: $(addsuffix .test, $(TESTS))
 
 test-examples: $(addsuffix .test, $(EXAMPLES))
 
-test-bootstrapped: test-boostrapped-hello
+test-bootstrapped: test-bootstrapped-hello
 
 clean: clean-tests clean-examples clean-bootstrap
 
@@ -32,7 +32,7 @@ clean-examples:  $(addsuffix .clean, $(EXAMPLES))
 .PHONY:
 	all test test-ci test-tests test-examples test-bootstrap\
 	clean clean-all clean-tests clean-examples clean-build clean-bootstrap\
-	time-bootstrap check-bootstrap test-bootstrapped test-boostrapped-hello\
+	time-bootstrap check-bootstrap test-bootstrapped test-bootstrapped-hello\
 	$(addsuffix .clean, $(TESTS) $(EXAMPLES)) $(addsuffix .test, $(TESTS) $(EXAMPLES))
 
 #-------------------------------------------------------------------------------
@@ -82,5 +82,5 @@ time-bootstrap:
 check-bootstrap:
 	cd examples/bootstrap && ./check.sh
 
-test-boostrapped-hello:
+test-bootstrapped-hello:
 	cd examples/hello && ./bootstrapped-test.sh
diff --git a/src/lake/examples/scripts/test.sh b/src/lake/examples/scripts/test.sh
index bb08f820ac..cf4f2d3f1d 100755
--- a/src/lake/examples/scripts/test.sh
+++ b/src/lake/examples/scripts/test.sh
@@ -15,7 +15,7 @@ $LAKE script run greet --me | tee -a produced.out
 $LAKE script doc greet | tee -a produced.out
 $LAKE script run hello | tee -a produced.out
 $LAKE script run dep/hello | tee -a produced.out
-# Test that non-indentifier names work
+# Test that non-identifier names work
 # https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Running.20.60lake.60.20scripts.20from.20the.20command.20line/near/446944450
 $LAKE script run say-goodbye | tee -a produced.out
 ($LAKE script run nonexistent 2>&1 | tee -a produced.out) && exit 1 || true
diff --git a/src/lake/schemas/lakefile-toml-schema.json b/src/lake/schemas/lakefile-toml-schema.json
index 301424c705..7ca0fda41f 100644
--- a/src/lake/schemas/lakefile-toml-schema.json
+++ b/src/lake/schemas/lakefile-toml-schema.json
@@ -326,7 +326,7 @@
                         "object"
                     ],
                     "default": "*",
-                    "description": "Includes only the files from the directory whose paths satisify this pattern.\n\nFormat: Either `\"*\"`, or a recursive object with one of the following properties at every layer:\n- `path`: String pattern matching the path.\n- `extension`: String pattern matching the extension of the file in the path.\n- `fileName`: String pattern matching the name of the file in the path.\n- `not`: Negate a path pattern.\n- `any`: Match any of an array of path patterns.\n- `all`: Match all of an array of path patterns.\n\nString patterns have the following format: Either `\"*\"`, an array of all strings that are a match, or a recursive object with one of the following properties at every layer:\n- `startsWith`: Denotes a prefix string of all strings that are a match.\n- `endsWith`: Denotes a suffix string of all strings that are a match.\n- `not`: Negate a string pattern.\n- `any`: Match any of an array of string patterns.\n- `all`: Match all of an array of string patterns."
+                    "description": "Includes only the files from the directory whose paths satisfy this pattern.\n\nFormat: Either `\"*\"`, or a recursive object with one of the following properties at every layer:\n- `path`: String pattern matching the path.\n- `extension`: String pattern matching the extension of the file in the path.\n- `fileName`: String pattern matching the name of the file in the path.\n- `not`: Negate a path pattern.\n- `any`: Match any of an array of path patterns.\n- `all`: Match all of an array of path patterns.\n\nString patterns have the following format: Either `\"*\"`, an array of all strings that are a match, or a recursive object with one of the following properties at every layer:\n- `startsWith`: Denotes a prefix string of all strings that are a match.\n- `endsWith`: Denotes a suffix string of all strings that are a match.\n- `not`: Negate a string pattern.\n- `any`: Match any of an array of string patterns.\n- `all`: Match all of an array of string patterns."
                 }
             },
             "required": [
diff --git a/src/lake/tests/toml/tests/valid/array/hetergeneous.json b/src/lake/tests/toml/tests/valid/array/heterogeneous.json
similarity index 100%
rename from src/lake/tests/toml/tests/valid/array/hetergeneous.json
rename to src/lake/tests/toml/tests/valid/array/heterogeneous.json
diff --git a/src/lake/tests/toml/tests/valid/array/hetergeneous.toml b/src/lake/tests/toml/tests/valid/array/heterogeneous.toml
similarity index 100%
rename from src/lake/tests/toml/tests/valid/array/hetergeneous.toml
rename to src/lake/tests/toml/tests/valid/array/heterogeneous.toml
diff --git a/tests/lean/interactive/hoverBinderUndescore.lean b/tests/lean/interactive/hoverBinderUnderscore.lean
similarity index 100%
rename from tests/lean/interactive/hoverBinderUndescore.lean
rename to tests/lean/interactive/hoverBinderUnderscore.lean
diff --git a/tests/lean/interactive/hoverBinderUndescore.lean.expected.out b/tests/lean/interactive/hoverBinderUnderscore.lean.expected.out
similarity index 94%
rename from tests/lean/interactive/hoverBinderUndescore.lean.expected.out
rename to tests/lean/interactive/hoverBinderUnderscore.lean.expected.out
index f254328c43..f9b6bba6f4 100644
--- a/tests/lean/interactive/hoverBinderUndescore.lean.expected.out
+++ b/tests/lean/interactive/hoverBinderUnderscore.lean.expected.out
@@ -1,4 +1,4 @@
-{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
+{"textDocument": {"uri": "file:///hoverBinderUnderscore.lean"},
  "position": {"line": 1, "character": 5}}
 {"range":
  {"start": {"line": 1, "character": 5}, "end": {"line": 1, "character": 6}},
@@ -6,7 +6,7 @@
  {"value":
   "```lean\nNat\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
-{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
+{"textDocument": {"uri": "file:///hoverBinderUnderscore.lean"},
  "position": {"line": 1, "character": 7}}
 {"range":
  {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 8}},
@@ -14,7 +14,7 @@
  {"value":
   "```lean\nBool\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
-{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
+{"textDocument": {"uri": "file:///hoverBinderUnderscore.lean"},
  "position": {"line": 6, "character": 6}}
 {"range":
  {"start": {"line": 6, "character": 6}, "end": {"line": 6, "character": 7}},
@@ -22,7 +22,7 @@
  {"value":
   "```lean\nNat\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
-{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
+{"textDocument": {"uri": "file:///hoverBinderUnderscore.lean"},
  "position": {"line": 6, "character": 8}}
 {"range":
  {"start": {"line": 6, "character": 8}, "end": {"line": 6, "character": 9}},
@@ -30,7 +30,7 @@
  {"value":
   "```lean\nBool\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
-{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
+{"textDocument": {"uri": "file:///hoverBinderUnderscore.lean"},
  "position": {"line": 11, "character": 6}}
 {"range":
  {"start": {"line": 11, "character": 6}, "end": {"line": 11, "character": 7}},
@@ -38,7 +38,7 @@
  {"value":
   "```lean\nNat\n```\n***\nA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.\nFor example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.\n\nThe way this works is that holes create fresh metavariables.\nThe elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.\nThis is often known as *unification*.\n\nNormally, all holes must be solved for. However, there are a few contexts where this is not necessary:\n* In `match` patterns, holes are catch-all patterns.\n* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.\n\nRelated concept: implicit parameters are automatically filled in with holes during the elaboration process.\n\nSee also `?m` syntax (synthetic holes).\n",
   "kind": "markdown"}}
-{"textDocument": {"uri": "file:///hoverBinderUndescore.lean"},
+{"textDocument": {"uri": "file:///hoverBinderUnderscore.lean"},
  "position": {"line": 11, "character": 8}}
 {"range":
  {"start": {"line": 11, "character": 8}, "end": {"line": 11, "character": 9}},
diff --git a/tests/lean/motiveNotTypeCorect.lean b/tests/lean/motiveNotTypeCorrect.lean
similarity index 100%
rename from tests/lean/motiveNotTypeCorect.lean
rename to tests/lean/motiveNotTypeCorrect.lean
diff --git a/tests/lean/motiveNotTypeCorect.lean.expected.out b/tests/lean/motiveNotTypeCorrect.lean.expected.out
similarity index 88%
rename from tests/lean/motiveNotTypeCorect.lean.expected.out
rename to tests/lean/motiveNotTypeCorrect.lean.expected.out
index 5e324f83e0..61e4e0bfb6 100644
--- a/tests/lean/motiveNotTypeCorect.lean.expected.out
+++ b/tests/lean/motiveNotTypeCorrect.lean.expected.out
@@ -1,4 +1,4 @@
-motiveNotTypeCorect.lean:7:6-7:7: error: Tactic `rewrite` failed: motive is not type correct:
+motiveNotTypeCorrect.lean:7:6-7:7: error: Tactic `rewrite` failed: motive is not type correct:
   fun _a => P _a d
 Error: Application type mismatch: The argument
   d
@@ -19,7 +19,7 @@ h : f t = t
 d : D (f t)
 P : (t : Nat) → D t → Prop
 ⊢ P (f t) d
-motiveNotTypeCorect.lean:18:8-18:9: error: Tactic `rewrite` failed: Motive is dependent:
+motiveNotTypeCorrect.lean:18:8-18:9: error: Tactic `rewrite` failed: Motive is dependent:
   fun _a => A _a
 
 Note: The rewrite tactic cannot substitute terms on which the type of the target expression depends. The type of the expression
diff --git a/tests/lean/run/8815.lean b/tests/lean/run/8815.lean
index 8c4e6068b6..58c5a2d6d2 100644
--- a/tests/lean/run/8815.lean
+++ b/tests/lean/run/8815.lean
@@ -34,7 +34,7 @@ example : f 0 > 0 := by simp!
 
 
 -- NB: simp! disables all warnings, not just for declarations to unfold
--- Mild bug, but not a regresion.
+-- Mild bug, but not a regression.
 
 /--
 error: unsolved goals
diff --git a/tests/lean/run/bv_decide_rewriter_ac_nf.lean b/tests/lean/run/bv_decide_rewriter_ac_nf.lean
index 345c7c43ab..a1d3c5d847 100644
--- a/tests/lean/run/bv_decide_rewriter_ac_nf.lean
+++ b/tests/lean/run/bv_decide_rewriter_ac_nf.lean
@@ -90,7 +90,7 @@ local macro "repeat_mul" n:num "with" x:term  : term =>
 This test showcases that the runtime of `bv_ac_nf` is not a bottleneck:
 * Testing with 100 as the repetition amount runs in about 200ms with `skipKernelTC` set,
     or ~3.3 seconds without (c.q. 2.3s for `ac_rfl`), and
-* Putting in 125 for the repetition amount wil give a `maximum recursion depth has been reached`
+* Putting in 125 for the repetition amount will give a `maximum recursion depth has been reached`
     error thrown by simp anyway, so the runtime is not a limiting factor to begin with.
 -/
 set_option debug.skipKernelTC true in
diff --git a/tests/lean/run/defaulValueParamIssue.lean b/tests/lean/run/defaultValueParamIssue.lean
similarity index 100%
rename from tests/lean/run/defaulValueParamIssue.lean
rename to tests/lean/run/defaultValueParamIssue.lean
diff --git a/tests/lean/run/explictOpenDeclIssue.lean b/tests/lean/run/explicitOpenDeclIssue.lean
similarity index 100%
rename from tests/lean/run/explictOpenDeclIssue.lean
rename to tests/lean/run/explicitOpenDeclIssue.lean
diff --git a/tests/lean/run/funind_structural.lean b/tests/lean/run/funind_structural.lean
index 918412a006..64a6f836b7 100644
--- a/tests/lean/run/funind_structural.lean
+++ b/tests/lean/run/funind_structural.lean
@@ -61,7 +61,7 @@ info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α 
 #guard_msgs in
 #check zip.induct
 
-/-- Lets try ot use it! -/
+/-- Let's try to use it! -/
 theorem zip_length {α β} (xs : List α) (ys : List β) :
     (zip xs ys).length = xs.length.min ys.length := by
   induction xs, ys using zip.induct
diff --git a/tests/lean/run/grind_nochrono.lean b/tests/lean/run/grind_nochrono.lean
index cad5602a2b..7746180035 100644
--- a/tests/lean/run/grind_nochrono.lean
+++ b/tests/lean/run/grind_nochrono.lean
@@ -1,6 +1,6 @@
 module
 -- In the following test, the first 8 case-splits are irrelevant,
--- and non-choronological backtracking is used to avoid searching
+-- and non-chronological backtracking is used to avoid searching
 -- (2^8 - 1) irrelevant branches
 /--
 trace: [grind.split] p8 ∨ q8, generation: 0
diff --git a/tests/lean/run/hmulDefaultIntance.lean b/tests/lean/run/hmulDefaultInstance.lean
similarity index 100%
rename from tests/lean/run/hmulDefaultIntance.lean
rename to tests/lean/run/hmulDefaultInstance.lean
diff --git a/tests/lean/run/issue8939.lean b/tests/lean/run/issue8939.lean
index a090b07cd9..515ae71f01 100644
--- a/tests/lean/run/issue8939.lean
+++ b/tests/lean/run/issue8939.lean
@@ -43,8 +43,8 @@ end Test3
 
 namespace Test4
 
--- This checks that when unfolding abstraced proofs, we do not unfold function calls
--- that were actuallly there, like the one to `Function.cons` below
+-- This checks that when unfolding abstracted proofs, we do not unfold function calls
+-- that were actually there, like the one to `Function.cons` below
 
 /--
 error: failed to infer structural recursion:
diff --git a/tests/lean/traceStateBactracking.lean b/tests/lean/traceStateBacktracking.lean
similarity index 100%
rename from tests/lean/traceStateBactracking.lean
rename to tests/lean/traceStateBacktracking.lean
diff --git a/tests/lean/traceStateBactracking.lean.expected.out b/tests/lean/traceStateBacktracking.lean.expected.out
similarity index 100%
rename from tests/lean/traceStateBactracking.lean.expected.out
rename to tests/lean/traceStateBacktracking.lean.expected.out