diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean
index 350dd49257..fb9a6b6fa3 100644
--- a/src/Lean/Compiler/IR/EmitLLVM.lean
+++ b/src/Lean/Compiler/IR/EmitLLVM.lean
@@ -1044,7 +1044,7 @@ mutual
 partial def emitCase (builder : LLVM.Builder llvmctx)
     (x : VarId) (xType : IRType) (alts : Array Alt) : M llvmctx Unit := do
   let oldBB ← LLVM.getInsertBlock builder
-  -- NOTE: In this context, 'Zext' versus 'Sext' have a meaninful semantic difference.
+  -- NOTE: In this context, 'Zext' versus 'Sext' have a meaningful semantic difference.
   --       We perform a zero extend so that one-bit tags of `0/-1` actually extend to `0/1`
   --       in 64-bit space.
   let tag ← emitTag builder x xType
diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean
index aab8af752c..7352601f6e 100644
--- a/src/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -86,7 +86,7 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
 def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask :=
   eraseProjIncForAux y bs (mkArray n none) #[]
 
-/-- Replace `reuse x ctor ...` with `ctor ...`, and remoce `dec x` -/
+/-- Replace `reuse x ctor ...` with `ctor ...`, and remove `dec x` -/
 partial def reuseToCtor (x : VarId) : FnBody → FnBody
   | FnBody.dec y n c p b   =>
     if x == y then b -- n must be 1 since `x := reset ...`
@@ -236,7 +236,7 @@ def mkFastPath (x y : VarId) (mask : Mask) (b : FnBody) : M FnBody := do
 partial def expand (mainFn : FnBody → Array FnBody → M FnBody)
     (bs : Array FnBody) (x : VarId) (n : Nat) (y : VarId) (b : FnBody) : M FnBody := do
   let (bs, mask) := eraseProjIncFor n y bs
-  /- Remark: we may be duplicting variable/JP indices. That is, `bSlow` and `bFast` may
+  /- Remark: we may be duplicating variable/JP indices. That is, `bSlow` and `bFast` may
      have duplicate indices. We run `normalizeIds` to fix the ids after we have expand them. -/
   let bSlow      := mkSlowPath x y mask b
   let bFast ← mkFastPath x y mask b
diff --git a/src/Lean/Compiler/IR/ResetReuse.lean b/src/Lean/Compiler/IR/ResetReuse.lean
index 9566eb5758..a358f3afcc 100644
--- a/src/Lean/Compiler/IR/ResetReuse.lean
+++ b/src/Lean/Compiler/IR/ResetReuse.lean
@@ -9,7 +9,7 @@ import Lean.Compiler.IR.Format
 
 namespace Lean.IR.ResetReuse
 /-! Remark: the insertResetReuse transformation is applied before we have
-   inserted `inc/dec` instructions, and perfomed lower level optimizations
+   inserted `inc/dec` instructions, and performed lower level optimizations
    that introduce the instructions `release` and `set`. -/
 
 /-! Remark: the functions `S`, `D` and `R` defined here implement the
diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean
index 009ffc7ae7..a0c6a21224 100644
--- a/src/Lean/Compiler/LCNF/Basic.lean
+++ b/src/Lean/Compiler/LCNF/Basic.lean
@@ -471,7 +471,7 @@ structure Decl where
   of this kind. See `DefinitionSafety`.
   `partial` and `unsafe` functions may not be terminating, but Lean
   functions terminate, and some static analyzers exploit this
-  fact. So, we use the following semantics. Suppose whe hav a (large) natural
+  fact. So, we use the following semantics. Suppose we have a (large) natural
   number `C`. We consider a nondeterministic model for computation of Lean expressions as
   follows:
   Each call to a partial/unsafe function uses up one "recursion token".
@@ -490,7 +490,7 @@ structure Decl where
   safe : Bool := true
   /--
   We store the inline attribute at LCNF declarations to make sure we can set them for
-  auxliary declarations created during compilation.
+  auxiliary declarations created during compilation.
   -/
   inlineAttr? : Option InlineAttributeKind
   deriving Inhabited, BEq
diff --git a/src/Lean/Compiler/LCNF/Closure.lean b/src/Lean/Compiler/LCNF/Closure.lean
index 788e99f61b..450e4ef182 100644
--- a/src/Lean/Compiler/LCNF/Closure.lean
+++ b/src/Lean/Compiler/LCNF/Closure.lean
@@ -24,7 +24,7 @@ structure Context where
   inScope : FVarId → Bool
   /--
   If `abstract x` returns `true`, we convert `x` into a closure parameter. Otherwise,
-  we collect the dependecies in the `let`/`fun`-declaration too, and include the declaration in the closure.
+  we collect the dependencies in the `let`/`fun`-declaration too, and include the declaration in the closure.
   Remark: the lambda lifting pass abstracts all `let`/`fun`-declarations.
   -/
   abstract : FVarId → Bool
diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
index 160a574c77..fc15d59352 100644
--- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
@@ -26,7 +26,7 @@ inductive Value where
   -/
   | top
   /--
-  A certian consructor with a certain sets of parameters is possible.
+  A certain constructor with a certain sets of parameters is possible.
   -/
   | ctor (i : Name) (vs : Array Value)
   /--
@@ -531,7 +531,7 @@ partial def inferMain : InterpM Unit := do
     return ()
 
 /--
-Use the information produced by the abstract interpeter to:
+Use the information produced by the abstract interpreter to:
 - Eliminate branches that we know cannot be hit
 - Eliminate values that we know have to be constants.
 -/
diff --git a/src/Lean/Compiler/LCNF/FloatLetIn.lean b/src/Lean/Compiler/LCNF/FloatLetIn.lean
index 9849a20c81..174a9d4776 100644
--- a/src/Lean/Compiler/LCNF/FloatLetIn.lean
+++ b/src/Lean/Compiler/LCNF/FloatLetIn.lean
@@ -187,7 +187,7 @@ Will:
     | n => x * y
     | m => z
     ```
-    If we are at `y` `x` is alreayd marked to be floated into `n` as well.
+    If we are at `y` `x` is already marked to be floated into `n` as well.
   - if there hasn't be a decision yet, that is they are marked with `.unknown` we float
     them into the same arm as the current value:
     ```
@@ -211,7 +211,7 @@ Will:
     When we visit `a` `x` is now marked as getting moved into `n` but since it also occurs
     in `a` which wants to be moved somewhere else we will instead decide to not move `x`
     at all.
-  - if they are meant to be floated somewhere else decide that they wont get floated:
+  - if they are meant to be floated somewhere else decide that they won't get floated:
     ```
     let x := ...
     let y := x + z
@@ -234,7 +234,7 @@ where
       modify fun s => { s with decision := s.decision.insert fvar arm }
 
 /--
-Iterate throgh `decl`, pushing local declarations that are only used in one
+Iterate through `decl`, pushing local declarations that are only used in one
 control flow arm into said arm in order to avoid useless computations.
 -/
 partial def floatLetIn (decl : Decl) : CompilerM Decl := do
diff --git a/src/Lean/Compiler/LCNF/JoinPoints.lean b/src/Lean/Compiler/LCNF/JoinPoints.lean
index 6acbb730af..09dfdf2341 100644
--- a/src/Lean/Compiler/LCNF/JoinPoints.lean
+++ b/src/Lean/Compiler/LCNF/JoinPoints.lean
@@ -342,7 +342,7 @@ def mergeJpContextIfNecessary (jp : FVarId) : ExtendM Unit := do
 
 /--
 We call this whenever we enter a new local function. It clears both the
-current join point and the list of candidates since we cant lift join
+current join point and the list of candidates since we can't lift join
 points outside of functions as explained in `mergeJpContextIfNecessary`.
 -/
 def withNewFunScope (decl : FunDecl) (x : ExtendM α): ExtendM α := do
diff --git a/src/Lean/Compiler/LCNF/Level.lean b/src/Lean/Compiler/LCNF/Level.lean
index cd4984d80e..4275ce9af0 100644
--- a/src/Lean/Compiler/LCNF/Level.lean
+++ b/src/Lean/Compiler/LCNF/Level.lean
@@ -33,7 +33,7 @@ structure State where
   /-- Parameters that have been normalized. -/
   paramNames : Array Name := #[]
 
-/-- Monad for the universe leve normalizer -/
+/-- Monad for the universe level normalizer -/
 abbrev M := StateM State
 
 /--
diff --git a/src/Lean/Compiler/LCNF/ReduceArity.lean b/src/Lean/Compiler/LCNF/ReduceArity.lean
index 9b862b81e5..4518494b96 100644
--- a/src/Lean/Compiler/LCNF/ReduceArity.lean
+++ b/src/Lean/Compiler/LCNF/ReduceArity.lean
@@ -13,7 +13,7 @@ namespace Lean.Compiler.LCNF
 # Function arity reduction
 
 This module finds "used" parameters in a declaration, and then
-create an auxliary declaration that contains only used parameters.
+create an auxiliary declaration that contains only used parameters.
 For example:
 ```
 def f (x y : Nat) : Nat :=
diff --git a/src/Lean/Compiler/LCNF/Simp/JpCases.lean b/src/Lean/Compiler/LCNF/Simp/JpCases.lean
index a012e1842f..962fb2fc36 100644
--- a/src/Lean/Compiler/LCNF/Simp/JpCases.lean
+++ b/src/Lean/Compiler/LCNF/Simp/JpCases.lean
@@ -105,7 +105,7 @@ abbrev Ctor2JpCasesAlt := FVarIdMap (NameMap JpCasesAlt)
 
 open Internalize in
 /--
-Construct an auxiliary join point for a particular alternative in a join-point that satifies `isJpCases?`.
+Construct an auxiliary join point for a particular alternative in a join-point that satisfies `isJpCases?`.
 - `decls` is the prefix (before the `cases`). See `isJpCases?`.
 - `params` are the parameters of the main join point that satisfies `isJpCases?`.
 - `targetParamIdx` is the index of the parameter that we are expanding to `fields`
@@ -149,7 +149,7 @@ private def mkJmpArgsAtJp (params : Array Param) (targetParamIdx : Nat) (fields
 
 /--
 Try to optimize `jpCases` join points.
-We say a join point is a `jpCases` when it satifies the predicate `isJpCases`.
+We say a join point is a `jpCases` when it satisfies the predicate `isJpCases`.
 If we have a jump to `jpCases` with a constructor, then we can optimize the code by creating an new join point for
 the constructor.
 Example: suppose we have
diff --git a/src/Lean/Compiler/LCNF/Simp/SimpM.lean b/src/Lean/Compiler/LCNF/Simp/SimpM.lean
index 59ae4baa69..4deab43c23 100644
--- a/src/Lean/Compiler/LCNF/Simp/SimpM.lean
+++ b/src/Lean/Compiler/LCNF/Simp/SimpM.lean
@@ -139,7 +139,7 @@ where
     return numOccs
 
 /--
-Similar to the default `Lean.withIncRecDepth`, but include the `inlineStack` in the error messsage.
+Similar to the default `Lean.withIncRecDepth`, but include the `inlineStack` in the error message.
 -/
 @[inline] def withIncRecDepth (x : SimpM α) : SimpM α := do
   let curr ← MonadRecDepth.getRecDepth
diff --git a/src/Lean/Compiler/LCNF/SpecInfo.lean b/src/Lean/Compiler/LCNF/SpecInfo.lean
index d0553efe66..fa6d6e4b03 100644
--- a/src/Lean/Compiler/LCNF/SpecInfo.lean
+++ b/src/Lean/Compiler/LCNF/SpecInfo.lean
@@ -103,7 +103,7 @@ private def isNoSpecType (env : Environment) (type : Expr) : Bool :=
 *Note*: `fixedNeutral` must have forward dependencies.
 
 The code specializer consider a `fixedNeutral` parameter during code specialization
-only if it contains forward dependecies that are tagged as `.user`, `.fixedHO`, or `.fixedInst`.
+only if it contains forward dependencies that are tagged as `.user`, `.fixedHO`, or `.fixedInst`.
 The motivation is to minimize the number of code specializations that have little or no impact on
 performance. For example, let's consider the function.
 ```
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 46bdb50621..263755ee62 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -114,7 +114,7 @@ protected def toString : JsonNumber → String
 protected def shiftl : JsonNumber → Nat → JsonNumber
   -- if s ≤ e, then 10 ^ (s - e) = 1, and hence the mantissa remains unchanged.
   -- otherwise, the expression pads the mantissa with zeroes
-  -- to accomodate for the remaining places to shift.
+  -- to accommodate for the remaining places to shift.
   | ⟨m, e⟩, s => ⟨m * (10 ^ (s - e) : Nat), e - s⟩
 
 -- shift a JsonNumber by a specified amount of places to the right
diff --git a/src/Lean/Data/Lsp/CodeActions.lean b/src/Lean/Data/Lsp/CodeActions.lean
index dcaa16c74f..6b4c97e685 100644
--- a/src/Lean/Data/Lsp/CodeActions.lean
+++ b/src/Lean/Data/Lsp/CodeActions.lean
@@ -83,7 +83,7 @@ structure CodeActionParams extends WorkDoneProgressParams, PartialResultParams w
   context      : CodeActionContext := {}
   deriving FromJson, ToJson
 
-/-- If the code action is disabled, this type gives the reson why. -/
+/-- If the code action is disabled, this type gives the reason why. -/
 structure CodeActionDisabled where
   reason : String
   deriving FromJson, ToJson
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index b97a959969..5ea21e385f 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -133,7 +133,7 @@ def isNum : Name → Bool
   | _      => false
 
 /--
-Return `true` if `n` contains a string part `s` that satifies `f`.
+Return `true` if `n` contains a string part `s` that satisfies `f`.
 
 Examples:
 ```
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 6f5ab35c6d..3921839065 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -132,7 +132,7 @@ private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=
 
 /--
 Convert `stx` into an array of `BinderView`s.
-`stx` must be an indentifier, `_`, `explicitBinder`, `implicitBinder`, `strictImplicitBinder`, or `instBinder`.
+`stx` must be an identifier, `_`, `explicitBinder`, `implicitBinder`, `strictImplicitBinder`, or `instBinder`.
 -/
 private def toBinderViews (stx : Syntax) : TermElabM (Array BinderView) := do
   let k := stx.getKind
@@ -233,7 +233,7 @@ def elabBindersEx (binders : Array Syntax) (k : Array (Syntax × Expr) → TermE
 
 /--
   Elaborate the given binders (i.e., `Syntax` objects for `bracketedBinder`),
-  update the local context, set of local instances, reset instance chache (if needed), and then
+  update the local context, set of local instances, reset instance cache (if needed), and then
   execute `k` with the updated context.
   The local context will only be included inside `k`.
 
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 482a45bec8..9d5cfddfcb 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -158,7 +158,7 @@ private def containsId (ids : Array (TSyntax [`ident, ``Parser.Term.hole])) (id
 /--
   Auxiliary method for processing binder annotation update commands: `variable (α)` and `variable {α}`.
   The argument `binder` is the binder of the `variable` command.
-  The method retuns an array containing the "residue", that is, variables that do not correspond to updates.
+  The method returns an array containing the "residue", that is, variables that do not correspond to updates.
   Recall that a `bracketedBinder` can be of the form `(x y)`.
   ```
   variable {α β : Type}
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index e2ff3e907d..9b9473157a 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -82,7 +82,7 @@ open Meta
     let type ← withSynthesize (mayPostpone := true) do
       let type ← elabType type
       if let some expectedType := expectedType? then
-        -- Recall that a similiar approach is used when elaborating applications
+        -- Recall that a similar approach is used when elaborating applications
         discard <| isDefEq expectedType type
       return type
     /-
diff --git a/src/Lean/Elab/Calc.lean b/src/Lean/Elab/Calc.lean
index 6240c45eab..0a33a18cb8 100644
--- a/src/Lean/Elab/Calc.lean
+++ b/src/Lean/Elab/Calc.lean
@@ -46,7 +46,7 @@ def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr)
 /--
 Adds a type annotation to a hole that occurs immediately at the beginning of the term.
 This is so that coercions can trigger when elaborating the term.
-See https://github.com/leanprover/lean4/issues/2040 for futher rationale.
+See https://github.com/leanprover/lean4/issues/2040 for further rationale.
 
 - `_ < 3` is annotated
 - `(_) < 3` is not, because it occurs after an atom
diff --git a/src/Lean/Elab/DeclarationRange.lean b/src/Lean/Elab/DeclarationRange.lean
index 9c403828ee..792879cc55 100644
--- a/src/Lean/Elab/DeclarationRange.lean
+++ b/src/Lean/Elab/DeclarationRange.lean
@@ -48,7 +48,7 @@ def getDeclarationSelectionRef (stx : Syntax) : Syntax :=
 
 
 /--
-  Store the `range` and `selectionRange` for `declName` where `stx` is the whole syntax object decribing `declName`.
+  Store the `range` and `selectionRange` for `declName` where `stx` is the whole syntax object describing `declName`.
   This method is for the builtin declarations only.
   User-defined commands should use `Lean.addDeclarationRanges` to store this information for their commands. -/
 def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) : m Unit := do
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 847791bc12..3865223498 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -501,7 +501,7 @@ def homogenize (c₁ c₂ : CodeBlock) : TermElabM (CodeBlock × CodeBlock) := d
 
 /--
 Extending code blocks with variable declarations: `let x : t := v` and `let x : t ← v`.
-We remove `x` from the collection of updated varibles.
+We remove `x` from the collection of updated variables.
 Remark: `stx` is the syntax for the declaration (e.g., `letDecl`), and `xs` are the variables
 declared by it. It is an array because we have let-declarations that declare multiple variables.
 Example: `let (x, y) := t`
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index f3d98d0587..a2f38eebc6 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -228,7 +228,7 @@ where
       type
 
 /--
-  Reorder contructor arguments to improve the effectiveness of the `fixedIndicesToParams` method.
+  Reorder constructor arguments to improve the effectiveness of the `fixedIndicesToParams` method.
 
   The idea is quite simple. Given a constructor type of the form
   ```
@@ -267,7 +267,7 @@ private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do
       let r ← mkForallFVars (bsPrefix ++ as) type
       /- `r` already contains the resulting type.
          To be able to produce more better error messages, we copy the first `bsPrefix.size` binder names from `C` to `r`.
-         This is important when some of contructor parameters were inferred using the auto-bound implicit feature.
+         This is important when some of constructor parameters were inferred using the auto-bound implicit feature.
          For example, in the following declaration.
          ```
           inductive Member : α → List α → Type u
@@ -549,7 +549,7 @@ private def checkResultingUniverses (views : Array InductiveView) (numParams : N
               /- Special case:
                  The constructor parameter `v` is at unverse level `?v+k` and
                  the resulting inductive universe level is `u'+k`, where `u'` is a parameter (or zero).
-                 Thus, `?v := u'` is the only choice for satisfying the universe contraint `?v+k <= u'+k`.
+                 Thus, `?v := u'` is the only choice for satisfying the universe constraint `?v+k <= u'+k`.
                  Note that, we still generate an error for cases where there is more than one of satisfying the constraint.
                  Examples:
                  -----------------------------------------------------------
diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index 7dc2dc5530..10ee3eb13b 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -52,7 +52,7 @@ partial def InfoTree.findInfo? (p : Info → Bool) (t : InfoTree) : Option Info
   | _ => none
 
 /-- Instantiate the holes on the given `tree` with the assignment table.
-(analoguous to instantiating the metavariables in an expression) -/
+(analogous to instantiating the metavariables in an expression) -/
 partial def InfoTree.substitute (tree : InfoTree) (assignment : PersistentHashMap MVarId InfoTree) : InfoTree :=
   match tree with
   | node i c => node i <| c.map (substitute · assignment)
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 22e5dd297c..1b183f9134 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -121,7 +121,7 @@ where
         This transformation was added to address issue #1155, and avoid an unnecessary dependency.
         In issue #1155, `discrType` was of the form `let _discr := OfNat.ofNat ... 0 ?m; ...`, and not removing
         the unnecessary `let-expr` was introducing an artificial dependency to `?m`.
-        TODO: make sure that even when this kind of artificial dependecy occurs we catch it before sending
+        TODO: make sure that even when this kind of artificial dependency occurs we catch it before sending
         the term to the kernel.
       -/
       let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr))
@@ -593,7 +593,7 @@ abbrev TopSortM := StateRefT TopSort.State TermElabM
 /--
   Topological sort. We need it because inaccessible patterns may contain pattern variables that are declared later.
   That is, processing patterns from left to right to do not guarantee that the pattern variables are collected in the
-  "right" order. "Right" here means pattern `x` must occur befor pattern `y` if `y`s type depends on `x`.
+  "right" order. "Right" here means pattern `x` must occur before pattern `y` if `y`s type depends on `x`.
 -/
 private partial def topSort (patternVars : Array Expr) : TermElabM (Array Expr) := do
   let (_, s) ← patternVars.mapM visit |>.run {}
@@ -1037,7 +1037,7 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
        | _ => pure ()
      ```
      If `synthesizeSyntheticMVarsNoPostponing`, the example above fails at `x.fst` because
-     the type of `x` is only available after we proces the last argument of `List.forM`.
+     the type of `x` is only available after we process the last argument of `List.forM`.
 
      We apply pending default types to make sure we can process examples such as
      ```
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index e37eb7d206..5d9bdd5d44 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -32,7 +32,7 @@ structure DefViewElabHeader where
   declName      : Name
   /-- Universe level parameter names explicitly provided by the user. -/
   levelNames    : List Name
-  /-- Syntax objects for the binders occurring befor `:`, we use them to populate the `InfoTree` when elaborating `valueStx`. -/
+  /-- Syntax objects for the binders occurring before `:`, we use them to populate the `InfoTree` when elaborating `valueStx`. -/
   binderIds     : Array Syntax
   /-- Number of parameters before `:`, it also includes auto-implicit parameters automatically added by Lean. -/
   numParams     : Nat
diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index ce6d9e2fbb..670143db69 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -319,7 +319,7 @@ builtin_initialize unfoldEqnExt : EnvExtension UnfoldEqnExtState ←
   ```
   declName x_1 ... x_n = body[x_1, ..., x_n]
   ```
-  The proof is constracted using the automatically generated equational theorems.
+  The proof is constructed using the automatically generated equational theorems.
   We basically keep splitting the `match` and `if-then-else` expressions in the right hand side
   until one of the equational theorems is applicable.
 -/
diff --git a/src/Lean/Elab/PreDefinition/Structural/Basic.lean b/src/Lean/Elab/PreDefinition/Structural/Basic.lean
index c3f392129e..4c99253e0b 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Basic.lean
@@ -54,7 +54,7 @@ def run (x : M α) (s : State := {}) : MetaM (α × State) :=
   the argument we are trying to recurse on, and it contains loose bound variables.
 
   We use this test to decide whether we should process a matcher-application as a regular
-  applicaton or not. That is, whether we should push the `below` argument should be affected by the matcher or not.
+  application or not. That is, whether we should push the `below` argument should be affected by the matcher or not.
   If `e` does not contain an application of the form `recFnName .. t ..`, then we know
   the recursion doesn't depend on any pattern variable in this matcher.
 -/
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 51cc3c1cc9..6a2cb23260 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -647,7 +647,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
 namespace DefaultFields
 
 structure Context where
-  -- We must search for default values overriden in derived structures
+  -- We must search for default values overridden in derived structures
   structs : Array Struct := #[]
   allStructNames : Array Name := #[]
   /--
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index f776f61f4a..1040c0e715 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -321,7 +321,7 @@ private def toVisibility (fieldInfo : StructureFieldInfo) : CoreM Visibility :=
 
 abbrev FieldMap := NameMap Expr -- Map from field name to expression representing the field
 
-/-- Reduce projetions of the structures in `structNames` -/
+/-- Reduce projections of the structures in `structNames` -/
 private def reduceProjs (e : Expr) (structNames : NameSet) : MetaM Expr :=
   let reduce (e : Expr) : MetaM TransformStep := do
     match (← reduceProjOf? e structNames.contains) with
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index d0bb07faef..9ed56cc650 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -274,7 +274,7 @@ private def throwStuckAtUniverseCnstr : TermElabM Unit := do
   ```
   Another benefit of using `withoutPostponingUniverseConstraints` is better error messages. Instead
   of getting a mysterious type mismatch constraint, we get a list of
-  universe contraints the system is stuck at.
+  universe constraints the system is stuck at.
 -/
 private def processPostponedUniverseContraints : TermElabM Unit := do
   unless (← processPostponed (mayPostpone := false) (exceptionOnFailure := true)) do
@@ -304,7 +304,7 @@ mutual
     `?m2` (for `by tac`). When `A` is resumed, it creates a new metavariable `?m3` for the nested `by ...` term in `A`.
     `?m3` is after `?m2` in the to-do list. Then, we execute `by tac` for synthesizing `?m2`, but its type depends on
     `?m3`. We have considered putting `?m3` at `?m2` place in the to-do list, but this is not super robust.
-    The ideal solution is to make sure a tactic "resolves" all pending metavariables nested in their local contex and target type
+    The ideal solution is to make sure a tactic "resolves" all pending metavariables nested in their local context and target type
     before starting tactic execution. The procedure would be a generalization of `runPendingTacticsAt`. We can try to combine
     it with `instantiateMVarDeclMVars` to make sure we do not perform two traversals.
     Regarding issue #1380, we addressed the issue by avoiding the elaboration postponement step. However, the same issue can happen
@@ -415,7 +415,7 @@ mutual
                Recall that we postponed `x` at `Prod.fst x` because its type it is not known.
                We the type of `x` may learn later its type and it may contain implicit and/or auto arguments.
                By disabling postponement, we are essentially giving up the opportunity of learning `x`s type
-               and assume it does not have implict and/or auto arguments. -/
+               and assume it does not have implicit and/or auto arguments. -/
             if ← withoutPostponing <| synthesizeSyntheticMVarsStep (postponeOnError := true) (runTactics := false) then
               loop ()
             else if ← synthesizeUsingDefault then
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 4e51e416f6..53032df034 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -261,7 +261,7 @@ def elabTermForApply (stx : Syntax) (mayPostpone := true) : TacticM Expr := do
     More complex solution:
       - We do not disable "error to sorry"
       - We elaborate term and check whether errors were produced
-      - If there are other tactic braches and there are errors, we remove the errors from the log, and throw a new error to force the tactic to backtrack.
+      - If there are other tactic branches and there are errors, we remove the errors from the log, and throw a new error to force the tactic to backtrack.
   -/
   withoutRecover <| elabTerm stx none mayPostpone
 
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index bbdcdb84fa..1e1a0fcbd1 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -395,7 +395,7 @@ private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Exp
     return (fvarIds.size, mvarId')
 
 /--
-Given `inductionAlts` of the fom
+Given `inductionAlts` of the form
 ```
 syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
 ```
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 18074aac93..44e1f7deb2 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -46,7 +46,7 @@ This can be set to
 - `implicit` --  `{x : α}`
 - `strict_implicit` -- `⦃x : α⦄`
 - `inst_implicit` -- `[x : α]`.
-- `aux_decl` -- Auxillary definitions are helper methods that
+- `aux_decl` -- Auxiliary definitions are helper methods that
   Lean generates. `aux_decl` is used for `_match`, `_fun_match`,
   `_let_match` and the self reference that appears in recursive pattern matching.
 
@@ -67,7 +67,7 @@ inductive BinderInfo where
   | default
   /-- Implicit binder annotation, e.g., `{x : α}` -/
   | implicit
-  /-- Strict implict binder annotation, e.g., `{{ x : α  }}` -/
+  /-- Strict implicit binder annotation, e.g., `{{ x : α }}` -/
   | strictImplicit
   /-- Local instance binder annotataion, e.g., `[Decidable α]` -/
   | instImplicit
@@ -321,7 +321,7 @@ inductive Expr where
   /--
   The `fvar` constructor represent free variables. These /free/ variable
   occurrences are not bound by an earlier `lam`, `forallE`, or `letE`
-  contructor and its binder exists in a local context only.
+  constructor and its binder exists in a local context only.
 
   Note that Lean uses the /locally nameless approach/. See [here](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf)
   for additional details.
@@ -1441,7 +1441,7 @@ partial def cleanupAnnotations (e : Expr) : Expr :=
   let e' := e.consumeMData.consumeTypeAnnotations
   if e' == e then e else cleanupAnnotations e'
 
-/-- Return true iff `e` contains a free variable which statisfies `p`. -/
+/-- Return true iff `e` contains a free variable which satisfies `p`. -/
 @[inline] def hasAnyFVar (e : Expr) (p : FVarId → Bool) : Bool :=
   let rec @[specialize] visit (e : Expr) := if !e.hasFVar then false else
     match e with
@@ -1754,21 +1754,21 @@ def isLHSGoal? (e : Expr) : Option Expr :=
 
 /--
 Polymorphic operation for generating unique/fresh free variable identifiers.
-It is available in any monad `m` that implements the inferface `MonadNameGenerator`.
+It is available in any monad `m` that implements the interface `MonadNameGenerator`.
 -/
 def mkFreshFVarId [Monad m] [MonadNameGenerator m] : m FVarId :=
   return { name := (← mkFreshId) }
 
 /--
 Polymorphic operation for generating unique/fresh metavariable identifiers.
-It is available in any monad `m` that implements the inferface `MonadNameGenerator`.
+It is available in any monad `m` that implements the interface `MonadNameGenerator`.
 -/
 def mkFreshMVarId [Monad m] [MonadNameGenerator m] : m MVarId :=
   return { name := (← mkFreshId) }
 
 /--
 Polymorphic operation for generating unique/fresh universe metavariable identifiers.
-It is available in any monad `m` that implements the inferface `MonadNameGenerator`.
+It is available in any monad `m` that implements the interface `MonadNameGenerator`.
 -/
 def mkFreshLMVarId [Monad m] [MonadNameGenerator m] : m LMVarId :=
   return { name := (← mkFreshId) }
diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean
index 167177f5a9..b47e4eaa0f 100644
--- a/src/Lean/Hygiene.lean
+++ b/src/Lean/Hygiene.lean
@@ -22,7 +22,7 @@ antiquotations, and if references to globals are prefixed with `_root_.`
 (which is not allowed to refer to a local variable)
 `Unhygienic` can also be seen as a model implementation of `MonadQuotation`
 (since it is completely hygienic as long as it is "run" only once and can
-assume that there are no other implentations in use, as is the case for the
+assume that there are no other implementations in use, as is the case for the
 elaboration monads that carry their macro scope state through the entire
 processing of a file). It uses the state monad to query and allocate the
 next macro scope, and uses the reader monad to store the stack of scopes
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index 74868ff827..83fc26db55 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -191,7 +191,7 @@ def mvarId! : Level → LMVarId
   | mvar mvarId => mvarId
   | _           => panic! "metavariable expected"
 
-/-- If result is true, then forall assignments `A` which assigns all parameters and metavariables occuring
+/-- If result is true, then forall assignments `A` which assigns all parameters and metavariables occurring
     in `l`, `l[A] != zero` -/
 def isNeverZero : Level → Bool
   | zero         => false
diff --git a/src/Lean/Meta/ACLt.lean b/src/Lean/Meta/ACLt.lean
index 122f1718d2..b5cd69d699 100644
--- a/src/Lean/Meta/ACLt.lean
+++ b/src/Lean/Meta/ACLt.lean
@@ -38,7 +38,7 @@ mutual
 
   Recall that an AC-compatible ordering if it is monotonic, well-founded, and total.
   Both KBO and LPO are AC-compatible. KBO is faster, but we do not cache the weight of
-  each expression in Lean 4. Even if we did, we would need to have a weight where implicit instace arguments are ignored.
+  each expression in Lean 4. Even if we did, we would need to have a weight where implicit instance arguments are ignored.
   So, we use a LPO-like term ordering.
 
   Remark: this method is used to implement ordered rewriting. We ignore implicit instance
@@ -120,7 +120,7 @@ where
     | .fvar id ..   => return Name.lt id.name b.fvarId!.name
     | .mvar id ..   => return Name.lt id.name b.mvarId!.name
     | .sort u ..    => return Level.normLt u b.sortLevel!
-    | .const n ..   => return Name.lt n b.constName! -- We igore the levels
+    | .const n ..   => return Name.lt n b.constName! -- We ignore the levels
     | .lit v ..     => return Literal.lt v b.litValue!
     -- Composite
     | .proj _ i e ..    => if i != b.projIdx! then return i < b.projIdx! else lt e b.projExpr!
diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean
index b76e65db62..da83060f82 100644
--- a/src/Lean/Meta/AbstractNestedProofs.lean
+++ b/src/Lean/Meta/AbstractNestedProofs.lean
@@ -36,7 +36,7 @@ private def mkAuxLemma (e : Expr) : M Expr := do
   let lemmaName ← mkAuxName (ctx.baseName ++ `proof) s.nextIdx
   modify fun s => { s with nextIdx := s.nextIdx + 1 }
   /- We turn on zeta-expansion to make sure we don't need to perform an expensive `check` step to
-     identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zeta expasion step.
+     identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zeta expansion step.
      It a benchmark created by @selsam, The extra `check` step was a bottleneck. -/
   mkAuxTheoremFor lemmaName e (zeta := true)
 
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 8309452256..39b0f4a408 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -553,7 +553,7 @@ def mkNumeral (type : Expr) (n : Nat) : MetaM Expr := do
 /--
   Return `a op b`, where `op` has name `opName` and is implemented using the typeclass `className`.
   This method assumes `a` and `b` have the same type, and typeclass `className` is heterogeneous.
-  Examples of supported clases: `HAdd`, `HSub`, `HMul`.
+  Examples of supported classes: `HAdd`, `HSub`, `HMul`.
   We use heterogeneous operators to ensure we have a uniform representation.
   -/
 private def mkBinaryOp (className : Name) (opName : Name) (a b : Expr) : MetaM Expr := do
@@ -574,7 +574,7 @@ def mkMul (a b : Expr) : MetaM Expr := mkBinaryOp ``HMul ``HMul.hMul a b
 /--
   Return `a r b`, where `r` has name `rName` and is implemented using the typeclass `className`.
   This method assumes `a` and `b` have the same type.
-  Examples of supported clases: `LE` and `LT`.
+  Examples of supported classes: `LE` and `LT`.
   We use heterogeneous operators to ensure we have a uniform representation.
   -/
 private def mkBinaryRel (className : Name) (rName : Name) (a b : Expr) : MetaM Expr := do
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 2ed7c55f2d..bfcce6d207 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -71,11 +71,11 @@ structure Config where
   constApprox        : Bool := false
   /--
     When the following flag is set,
-    `isDefEq` throws the exeption `Exeption.isDefEqStuck`
+    `isDefEq` throws the exception `Exeption.isDefEqStuck`
     whenever it encounters a constraint `?m ... =?= t` where
     `?m` is read only.
     This feature is useful for type class resolution where
-    we may want to notify the caller that the TC problem may be solveable
+    we may want to notify the caller that the TC problem may be solvable
     later after it assigns `?m`. -/
   isDefEqStuckEx     : Bool := false
   /--
@@ -185,7 +185,7 @@ structure InfoCacheKey where
   /--
     `nargs? = some n` if the cached information was computed assuming the function has arity `n`.
     If `nargs? = none`, then the cache information consumed the arrow type as much as possible
-    unsing the current transparency setting.
+    using the current transparency setting.
   X-/
   nargs?       : Option Nat
   deriving Inhabited, BEq
@@ -517,7 +517,7 @@ def findMVarDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl) :=
 
 /--
 Return `mvarId` declaration in the current metavariable context.
-Throw an exception if `mvarId` is not declarated in the current metavariable context.
+Throw an exception if `mvarId` is not declared in the current metavariable context.
 -/
 def _root_.Lean.MVarId.getDecl (mvarId : MVarId) : MetaM MetavarDecl := do
   match (← mvarId.findDecl?) with
@@ -529,7 +529,7 @@ def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do
   mvarId.getDecl
 
 /--
-Return `mvarId` kind. Throw an exception if `mvarId` is not declarated in the current metavariable context.
+Return `mvarId` kind. Throw an exception if `mvarId` is not declared in the current metavariable context.
 -/
 def _root_.Lean.MVarId.getKind (mvarId : MVarId) : MetaM MetavarKind :=
   return (← mvarId.getDecl).kind
@@ -538,7 +538,7 @@ def _root_.Lean.MVarId.getKind (mvarId : MVarId) : MetaM MetavarKind :=
 def getMVarDeclKind (mvarId : MVarId) : MetaM MetavarKind :=
   mvarId.getKind
 
-/-- Reture `true` if `e` is a synthetic (or synthetic opaque) metavariable -/
+/-- Return `true` if `e` is a synthetic (or synthetic opaque) metavariable -/
 def isSyntheticMVar (e : Expr) : MetaM Bool := do
   if e.isMVar then
      return (← e.mvarId!.getKind) matches .synthetic | .syntheticOpaque
@@ -778,16 +778,16 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 @[inline] def withTransparency (mode : TransparencyMode) : n α → n α :=
   mapMetaM <| withConfig (fun config => { config with transparency := mode })
 
-/-- `withDefault x` excutes `x` using the default transparency setting. -/
+/-- `withDefault x` executes `x` using the default transparency setting. -/
 @[inline] def withDefault (x : n α) : n α :=
   withTransparency TransparencyMode.default x
 
-/-- `withReducible x` excutes `x` using the reducible transparency setting. In this setting only definitions tagged as `[reducible]` are unfolded. -/
+/-- `withReducible x` executes `x` using the reducible transparency setting. In this setting only definitions tagged as `[reducible]` are unfolded. -/
 @[inline] def withReducible (x : n α) : n α :=
   withTransparency TransparencyMode.reducible x
 
 /--
-`withReducibleAndInstances x` excutes `x` using the `.instances` transparency setting. In this setting only definitions tagged as `[reducible]`
+`withReducibleAndInstances x` executes `x` using the `.instances` transparency setting. In this setting only definitions tagged as `[reducible]`
 or type class instances are unfolded.
 -/
 @[inline] def withReducibleAndInstances (x : n α) : n α :=
@@ -924,7 +924,7 @@ mutual
       dangling bound variables in the range `[j, fvars.size)`
     - if `reducing? == true` and `type` is not `forallE`, we use `whnf`.
     - when `type` is not a `forallE` nor it can't be reduced to one, we
-      excute the continuation `k`.
+      execute the continuation `k`.
 
     Here is an example that demonstrates the `reducing?`.
     Suppose we have
@@ -1048,7 +1048,7 @@ private def forallTelescopeReducingImp (type : Expr) (k : Array Expr → Expr 
 
 /--
   Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,
-  it reduces `A` and continues bulding the telescope if it is a `forall`. -/
+  it reduces `A` and continues building the telescope if it is a `forall`. -/
 def forallTelescopeReducing (type : Expr) (k : Array Expr → Expr → n α) : n α :=
   map2MetaM (fun k => forallTelescopeReducingImp type k) k
 
@@ -1599,7 +1599,7 @@ partial def processPostponed (mayPostpone : Bool := true) (exceptionOnFailure :=
     but it was not effective. It is more important to cache aggressively inside of a single `isDefEq`
     call because some of the heuristics create many similar subproblems.
     See issue #1102 for an example that triggers an exponential blowup if we don't use this more
-    aggresive form of caching.
+    aggressive form of caching.
   -/
   modifyDefEqCache fun _ => {}
   let postponed ← getResetPostponed
diff --git a/src/Lean/Meta/CollectMVars.lean b/src/Lean/Meta/CollectMVars.lean
index adc6c5c7c5..728deccccd 100644
--- a/src/Lean/Meta/CollectMVars.lean
+++ b/src/Lean/Meta/CollectMVars.lean
@@ -9,7 +9,7 @@ import Lean.Meta.Basic
 namespace Lean.Meta
 
 /--
-  Collect unassigned metavariables occuring in the given expression.
+  Collect unassigned metavariables occurring in the given expression.
 
   Remark: if `e` contains `?m` and there is a `t` assigned to `?m`, we
   collect unassigned metavariables occurring in `t`.
@@ -28,7 +28,7 @@ partial def collectMVars (e : Expr) : StateRefT CollectMVars.State MetaM Unit :=
     | none   => pure ()
     | some d => collectMVars (mkMVar d.mvarIdPending)
 
-/-- Return metavariables in occuring the given expression. See `collectMVars` -/
+/-- Return metavariables in occurring the given expression. See `collectMVars` -/
 def getMVars (e : Expr) : MetaM (Array MVarId) := do
   let (_, s) ← (collectMVars e).run {}
   pure s.result
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 8609250cfd..6fb8ccf081 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -131,7 +131,7 @@ instance : Inhabited (DiscrTree α s) where
     ```
     Decidable -> Eq -> * -> * -> * -> [Nat.decEq]
     ```
-    to the discrimination tree IF we ignored the implict `Nat` argument.
+    to the discrimination tree IF we ignored the implicit `Nat` argument.
     This would be BAD since **ALL** decidable equality instances would be in the same path.
     So, we index implicit arguments if they are types.
     This setting seems sensible for simplification theorems such as:
@@ -503,7 +503,7 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key s × Array
           we want `isDefEq` to throw an exception whenever it tries to assign
           a read-only metavariable.
           This feature is useful for type class resolution where
-          we may want to notify the caller that the TC problem may be solveable
+          we may want to notify the caller that the TC problem may be solvable
           later after it assigns `?m`.
           The method `DiscrTree.getUnify e` returns candidates `c` that may "unify" with `e`.
           That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (Add ?m)`
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 0a86085076..e1224b5d9e 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -183,7 +183,7 @@ inductive DefEqArgsFirstPassResult where
   Succeeded. The array `postponedImplicit` contains the position
   of the implicit arguments for which def-eq has been postponed.
   `postponedHO` contains the higher order output parameters, and parameters
-  that depend on them. They should be processed after the implict ones.
+  that depend on them. They should be processed after the implicit ones.
   `postponedHO` is used to handle applications involving functions that
   contain higher order output parameters. Example:
   ```lean
@@ -192,7 +192,7 @@ inductive DefEqArgsFirstPassResult where
     {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
     (xs : cont) → (i : idx) → (h : dom xs i) → elem
   ```
-  The argumengs `dom` and `h` must be processed after all implicit arguments
+  The arguments `dom` and `h` must be processed after all implicit arguments
   otherwise higher-order unification problems are generated. See issue #1299,
   when trying to solve
   ```
@@ -629,7 +629,7 @@ where
      let f (x : _) := pure "hello"; f ()
      ```
      with expected type `IO String`.
-     In this example, the following unification contraint is generated.
+     In this example, the following unification constraint is generated.
      ```
      ?m () String =?= IO String
      ```
@@ -649,7 +649,7 @@ where
      a **potential** dependency on `x`. By using constant approximation here, we are just saying the type of `f`
      does **not** depend on `x`. We claim this is a reasonable approximation in practice. Moreover, it is expected
      by any functional programmer used to non-dependently type languages (e.g., Haskell).
-     We distinguish the two cases above by using the field `numScopeArgs` at `MetavarDecl`. This fiels tracks
+     We distinguish the two cases above by using the field `numScopeArgs` at `MetavarDecl`. This field tracks
      how many metavariable arguments are representing dependencies.
 -/
 
@@ -735,7 +735,7 @@ mutual
             throwCheckAssignmentFailure -- It is not a pattern, then we fail and fall back to FO unification
           else if mvarDecl.lctx.isSubPrefixOf ctx.mvarDecl.lctx ctx.fvars then
             /- The local context of `mvar` - free variables being abstracted is a subprefix of the metavariable being assigned.
-               We "substract" variables being abstracted because we use `elimMVarDeps` -/
+               We "subtract" variables being abstracted because we use `elimMVarDeps` -/
             pure mvar
           else if mvarDecl.depth != (← getMCtx).depth || mvarDecl.kind.isSyntheticOpaque then
             traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId)
@@ -1034,7 +1034,7 @@ private def assignConst (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool :=
   ```
   ?m := fun y₁ ... y‌ⱼ => (fun y_{j+1} ... yₙ x₁ ... xᵢ => v)[a₁/y₁, .., aⱼ/yⱼ]
   ```
-  That is, after the longest prefix is found, we solve the contraint as the lhs was a pattern. See the definition of "pattern" above.
+  That is, after the longest prefix is found, we solve the constraint as the lhs was a pattern. See the definition of "pattern" above.
 -/
 private partial def processConstApprox (mvar : Expr) (args : Array Expr) (patternVarPrefix : Nat) (v : Expr) : MetaM Bool := do
   trace[Meta.isDefEq.constApprox] "{mvar} {args} := {v}"
@@ -1397,7 +1397,7 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
   if tNew != t then return some tNew
   /-
     If `assignSyntheticOpaque` is true, we must follow the delayed assignment.
-    Recall a delayed assignment `mvarId [xs] := mvarIdPending` is morally an assingment
+    Recall a delayed assignment `mvarId [xs] := mvarIdPending` is morally an assignment
     `mvarId := fun xs => mvarIdPending` where `xs` are free variables in the scope of `mvarIdPending`,
     but not in the scope of `mvarId`. We can only perform the abstraction when `mvarIdPending` has been fully synthesized.
     That is, `instantiateMVars (mkMVar mvarIdPending)` does not contain any expression metavariables.
@@ -1411,7 +1411,7 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
     We also have the delayed assignment `?m [xs] := ?n`, where `xs` are variables in the scope of `?n`,
     and this delayed assignment is morally `?m := fun xs => ?n`.
     Thus, we can reduce `?m as =?= s[as]` to `?n =?= s[as/xs]`, and solve it using `?n`'s local context.
-    This is more precise than simplying droping the arguments `as`.
+    This is more precise than simply dropping the arguments `as`.
   -/
   unless (← getConfig).assignSyntheticOpaque do return none
   let tArgs := t.getAppArgs
@@ -1688,7 +1688,7 @@ private def isDefEqProj : Expr → Expr → MetaM Bool
   | v, Expr.proj structName 0 s => isDefEqSingleton structName s v
   | _, _ => pure false
 where
-  /-- If `structName` is a structure with a single field and `(?m ...).1 =?= v`, then solve contraint as `?m ... =?= ⟨v⟩` -/
+  /-- If `structName` is a structure with a single field and `(?m ...).1 =?= v`, then solve constraint as `?m ... =?= ⟨v⟩` -/
   isDefEqSingleton (structName : Name) (s : Expr) (v : Expr) : MetaM Bool := do
     if isClass (← getEnv) structName then
       /-
@@ -1802,7 +1802,7 @@ private def getCachedResult (key : Expr × Expr) : MetaM LBool := do
 
 private def cacheResult (key : Expr × Expr) (result : Bool) : MetaM Unit := do
   /-
-  We must ensure that all assigned metavariables in the key are replaced by their current assingments.
+  We must ensure that all assigned metavariables in the key are replaced by their current assignments.
   Otherwise, the key is invalid after the assignment is "backtracked".
   See issue #1870 for an example.
   -/
diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index 7118a32058..71e23507e0 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -456,14 +456,14 @@ where
   /--
     this function changes the type of the pattern from the original type to the `below` version thereof.
     Most of the cases don't apply. In order to change the type and the pattern to be type correct, we don't
-    simply recursively change all occurrences, but rather, we recursively change occurences of the constructor.
+    simply recursively change all occurrences, but rather, we recursively change occurrences of the constructor.
     As such there are only a few cases:
     - the pattern is a constructor from the original type. Here we need to:
       - replace the constructor
       - copy original recursive patterns and convert them to below and reintroduce them in the correct position
       - turn original recursive patterns inaccessible
       - introduce free variables as needed.
-    - it is an `as` pattern. Here the contstructor could be hidden inside of it.
+    - it is an `as` pattern. Here the constructor could be hidden inside of it.
     - it is a variable. Here you we need to introduce a fresh variable of a different type.
   -/
   convertToBelow (indName : Name)
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index d3b784f965..f39ceef959 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -16,7 +16,7 @@ register_builtin_option synthInstance.checkSynthOrder : Bool := {
 }
 
 /-
-Note: we want to use iota reduction when indexing instaces. Otherwise,
+Note: we want to use iota reduction when indexing instances. Otherwise,
 we cannot elaborate examples such as
 ```
 inductive Ty where
diff --git a/src/Lean/Meta/KExprMap.lean b/src/Lean/Meta/KExprMap.lean
index d57b33df7d..55c61e9133 100644
--- a/src/Lean/Meta/KExprMap.lean
+++ b/src/Lean/Meta/KExprMap.lean
@@ -9,7 +9,7 @@ import Lean.Meta.Basic
 namespace Lean.Meta
 
 /--
-  A mapping that indentifies definitionally equal expressions.
+  A mapping that identifies definitionally equal expressions.
   We implement it as a mapping from `HeadIndex` to `AssocList Expr α`.
 
   Remark: this map may be quite inefficient if there are many `HeadIndex` collisions.
diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean
index 16dd830117..c674067bab 100644
--- a/src/Lean/Meta/Match/Basic.lean
+++ b/src/Lean/Meta/Match/Basic.lean
@@ -136,7 +136,7 @@ structure Alt where
   /-- `Syntax` object for providing position information -/
   ref       : Syntax
   /--
-  Orginal alternative index. Alternatives can be split, this index is the original
+  Original alternative index. Alternatives can be split, this index is the original
   position of the alternative that generated this one.
   -/
   idx       : Nat
diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean
index 2d0d6ecb02..aac439af6c 100644
--- a/src/Lean/Meta/Match/CaseValues.lean
+++ b/src/Lean/Meta/Match/CaseValues.lean
@@ -75,7 +75,7 @@ structure CaseValuesSubgoal where
   The type of `x` must have decidable equality.
 
   Remark: the last subgoal is for the "else" catchall case, and its `subst` is `{}`.
-  Remark: the fiels `newHs` has size 1 forall but the last subgoal.
+  Remark: the field `newHs` has size 1 forall but the last subgoal.
 
   If `substNewEqs = true`, then the new `h_i` equality hypotheses are substituted in the first `n` cases.
 -/
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 53af4b8688..b4ce227904 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -151,7 +151,7 @@ private def processSkipInaccessible (p : Problem) : Problem := Id.run do
   { p with alts := alts, vars := xs }
 
 /--
-If contraint is of the form `e ≋ x` where `x` is a free variable, reorient it
+If constraint is of the form `e ≋ x` where `x` is a free variable, reorient it
 as `x ≋ e` If
 - `x` is an `alt`-local declaration
 - `e` is not a free variable.
@@ -254,7 +254,7 @@ private def processAsPattern (p : Problem) : MetaM Problem := withGoalOf p do
     match alt.patterns with
     | .as fvarId p h :: ps =>
       /- We used to use `checkAndReplaceFVarId` here, but `x` and `fvarId` may have different types
-        when dependent types are beind used. Let's consider the repro for issue #471
+        when dependent types are being used. Let's consider the repro for issue #471
         ```
         inductive vec : Nat → Type
         | nil : vec 0
@@ -413,7 +413,7 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
          p.mvarId.cases x.fvarId!
        catch ex =>
          if p.alts.isEmpty then
-           /- If we have no alternatives and dependent pattern matching fails, then a "missing cases" error is bettern than a "stuck" error message. -/
+           /- If we have no alternatives and dependent pattern matching fails, then a "missing cases" error is better than a "stuck" error message. -/
            return none
          else
            throwCasesException p ex
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 3e2b76b972..909edfe87c 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -146,7 +146,7 @@ structure State where
   mvarId : MVarId            -- Goal representing the hypothesis
   xs  : List FVarId          -- Pattern variables for a previous case
   eqs : List FVarId          -- Equations to be processed
-  eqsNew : List FVarId := [] -- Simplied (already processed) equations
+  eqsNew : List FVarId := [] -- Simplified (already processed) equations
 
 abbrev M := StateRefT State MetaM
 
@@ -371,7 +371,7 @@ private abbrev ConvertM := ReaderT (FVarIdMap (Expr × Nat × Array Bool)) $ Sta
   Construct a proof for the splitter generated by `mkEquationsfor`.
   The proof uses the definition of the `match`-declaration as a template (argument `template`).
   - `alts` are free variables corresponding to alternatives of the `match` auxiliary declaration being processed.
-  - `altNews` are the new free variables which contains aditional hypotheses that ensure they are only used
+  - `altNews` are the new free variables which contains additional hypotheses that ensure they are only used
      when the previous overlapping alternatives are not applicable. -/
 private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (alts altsNew : Array Expr)
     (altsNewNumParams : Array Nat)
diff --git a/src/Lean/Meta/Match/Value.lean b/src/Lean/Meta/Match/Value.lean
index 39667cd59b..ba6e35927b 100644
--- a/src/Lean/Meta/Match/Value.lean
+++ b/src/Lean/Meta/Match/Value.lean
@@ -31,7 +31,7 @@ def isUIntPatLit (v : Expr) : Bool :=
   isUIntPatLit? v |>.isSome
 
 /--
-  The frontend expands uint numerals occurring in patterns into `UInt*.mk ..` contructor applications.
+  The frontend expands uint numerals occurring in patterns into `UInt*.mk ..` constructor applications.
   This method convert them back into `UInt*.ofNat ..` applications.
 -/
 def foldPatValue (v : Expr) : Expr :=
diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean
index 21ade50c12..3d87c7f971 100644
--- a/src/Lean/Meta/Offset.lean
+++ b/src/Lean/Meta/Offset.lean
@@ -113,7 +113,7 @@ private def mkOffset (e : Expr) (offset : Nat) : MetaM Expr := do
 def isDefEqOffset (s t : Expr) : MetaM LBool := do
   let ifNatExpr (x : MetaM LBool) : MetaM LBool := do
     let type ← inferType s
-    -- Remark: we use `withNewMCtxDepth` to make sure we don't assing metavariables when performing the `isDefEq` test
+    -- Remark: we use `withNewMCtxDepth` to make sure we don't assign metavariables when performing the `isDefEq` test
     if (← withNewMCtxDepth <| Meta.isExprDefEqAux type (mkConst ``Nat)) then
       x
     else
diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index d19e4673b0..23ac5268bb 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -52,7 +52,7 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
     let lctx           := mvarDecl.lctx
     let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
     withLCtx lctx mvarDecl.localInstances do
-      -- The followint two `let rec`s are being used to control the generated code size.
+      -- The following two `let rec`s are being used to control the generated code size.
       -- Then should be remove after we rewrite the compiler in Lean
       let rec pushPending (ids : List Name) (type? : Option Expr) (fmt : Format) : MetaM Format := do
         if ids.isEmpty then
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index ea502244b8..15f2bcc61a 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -601,7 +601,7 @@ it contains a regular parameter X that depends on an `out` parameter Y.
 
 Then, we execute type class resolution as usual.
 If it succeeds, and metavariables ?m_i have been assigned, we try to unify
-the original type `C a_1 ... a_n` witht the normalized one.
+the original type `C a_1 ... a_n` with the normalized one.
 -/
 
 private def preprocess (type : Expr) : MetaM Expr :=
@@ -697,7 +697,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
           trace[Meta.synthInstance] "result {result}"
           if (← assignOutParams result) then
             let result ← instantiateMVars result
-            /- We use `check` to propogate universe constraints implied by the `result`.
+            /- We use `check` to propagate universe constraints implied by the `result`.
                Recall that we use `allowLevelAssignments := true` which allows universe metavariables in the current depth to be assigned,
                but these assignments are discarded by `withNewMCtxDepth`.
 
diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean
index 418a77e2eb..3fd14009f4 100644
--- a/src/Lean/Meta/Tactic/Cases.lean
+++ b/src/Lean/Meta/Tactic/Cases.lean
@@ -168,7 +168,7 @@ private def hasIndepIndices (ctx : Context) : MetaM Bool := do
     /- One of the indices is not a free variable. -/
     return false
   else if ctx.majorTypeIndices.size.any fun i => i.any fun j => ctx.majorTypeIndices[i]! == ctx.majorTypeIndices[j]! then
-    /- An index ocurrs more than once -/
+    /- An index occurs more than once -/
     return false
   else
     (← getLCtx).allM fun decl =>
diff --git a/src/Lean/Meta/Tactic/Revert.lean b/src/Lean/Meta/Tactic/Revert.lean
index 1c4da42e33..c38195b682 100644
--- a/src/Lean/Meta/Tactic/Revert.lean
+++ b/src/Lean/Meta/Tactic/Revert.lean
@@ -32,7 +32,7 @@ def _root_.Lean.MVarId.revert (mvarId : MVarId) (fvarIds : Array FVarId) (preser
         toRevertNew := toRevertNew.push x
     let tag ← mvarId.getTag
     -- TODO: the following code can be optimized because `MetavarContext.revert` will compute `collectDeps` again.
-    -- We should factor out the relevat part
+    -- We should factor out the relevant part
 
     -- Set metavariable kind to natural to make sure `revert` will assign it.
     mvarId.setKind .natural
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 5a5d621d8b..4fca5307a0 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -66,7 +66,7 @@ private def mkImpCongr (src : Expr) (r₁ r₂ : Result) : MetaM Result := do
   let e := src.updateForallE! r₁.expr r₂.expr
   match r₁.proof?, r₂.proof? with
   | none,     none   => return { expr := e, proof? := none }
-  | _,        _      => return { expr := e, proof? := (← Meta.mkImpCongr (← r₁.getProof) (← r₂.getProof)) } -- TODO specialize if bootleneck
+  | _,        _      => return { expr := e, proof? := (← Meta.mkImpCongr (← r₁.getProof) (← r₂.getProof)) } -- TODO specialize if bottleneck
 
 /-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/
 def isOfNatNatLit (e : Expr) : Bool :=
diff --git a/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
index 17868a869d..48404047de 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
@@ -13,7 +13,7 @@ namespace Lean.Meta
 /--
   Data for user-defined theorems marked with the `congr` attribute.
 
-  This type should be confused with `CongrTheorem` which reprents different kinds of automatically
+  This type should be confused with `CongrTheorem` which represents different kinds of automatically
   generated congruence theorems. The `simp` tactic also uses some of them.
 -/
 structure SimpCongrTheorem where
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index 87cea99d20..7921193c44 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -51,7 +51,7 @@ instance : BEq Origin := ⟨(·.key == ·.key)⟩
 instance : Hashable Origin := ⟨(hash ·.key)⟩
 
 /-
-Note: we want to use iota reduction when indexing instaces. Otherwise,
+Note: we want to use iota reduction when indexing instances. Otherwise,
 we cannot use simp theorems such as
 ```
 @[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 847029153f..a76a15c772 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -164,7 +164,7 @@ where
     - `altEqs` are free variables of the form `h_altEq : discr = pattern`. `altEqs.size = numDiscrEqs ≤ discrs.size`
     This method executes `k altEqsNew subst` where
     - `altEqsNew` are fresh free variables of the form `h_altEqNew : discrVar = pattern`
-    - `subst` are terms of the form `h_eq.trans h_altEqNew : discr = pattern`. We use `subst` later to replace occurences of `h_altEq` with `h_eq.trans h_altEqNew`.
+    - `subst` are terms of the form `h_eq.trans h_altEqNew : discr = pattern`. We use `subst` later to replace occurrences of `h_altEq` with `h_eq.trans h_altEqNew`.
    -/
   withNewAltEqs (matcherInfo : MatcherInfo) (eqs : Array Expr) (altEqs : Array Expr) (k : Array Expr → Array Expr → MetaM Expr) : MetaM Expr := do
     let eqs' := (eqs.zip matcherInfo.discrInfos).filterMap fun (eq, info) => if info.hName?.isNone then none else some eq
diff --git a/src/Lean/Meta/Tactic/UnifyEq.lean b/src/Lean/Meta/Tactic/UnifyEq.lean
index 7bcf83f690..ee63627e67 100644
--- a/src/Lean/Meta/Tactic/UnifyEq.lean
+++ b/src/Lean/Meta/Tactic/UnifyEq.lean
@@ -7,9 +7,9 @@ import Lean.Meta.Tactic.Injection
 
 namespace Lean.Meta
 
-/-- Convert heterogeneous equality into a homegeneous one -/
+/-- Convert heterogeneous equality into a homogeneous one -/
 private def heqToEq' (mvarId : MVarId) (eqDecl : LocalDecl) : MetaM MVarId := do
-  /- Convert heterogeneous equality into a homegeneous one -/
+  /- Convert heterogeneous equality into a homogeneous one -/
   let prf    ← mkEqOfHEq (mkFVar eqDecl.fvarId)
   let aEqb   ← whnf (← inferType prf)
   let mvarId ← mvarId.assert eqDecl.userName aEqb prf
@@ -30,7 +30,7 @@ structure UnifyEqResult where
      - Normalize `a` and `b` using the current reducibility setting.
      - If `a` (`b`) is a free variable not occurring in `b` (`a`), replace it everywhere.
      - If `a` and `b` are distinct constructors, return `none` to indicate that the goal has been closed.
-     - If `a` and `b` are the same contructor, apply `injection`, the result contains the number of new equalities introduced in the goal.
+     - If `a` and `b` are the same constructor, apply `injection`, the result contains the number of new equalities introduced in the goal.
      - It also tries to apply the given `acyclic` method to try to close the goal.
        Remark: It is a parameter because `simp` uses `unifyEq?`, and `acyclic` depends on `simp`.
 -/
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index d4cfa085d9..4759521b74 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -416,7 +416,7 @@ private def whnfMatcher (e : Expr) : MetaM Expr := do
   /- When reducing `match` expressions, if the reducibility setting is at `TransparencyMode.reducible`,
      we increase it to `TransparencyMode.instances`. We use the `TransparencyMode.reducible` in many places (e.g., `simp`),
      and this setting prevents us from reducing `match` expressions where the discriminants are terms such as `OfNat.ofNat α n inst`.
-     For example, `simp [Int.div]` will not unfold the application `Int.div 2 1` occuring in the target.
+     For example, `simp [Int.div]` will not unfold the application `Int.div 2 1` occurring in the target.
 
      TODO: consider other solutions; investigate whether the solution above produces counterintuitive behavior.  -/
   let mut transparency ← getTransparency
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 9b1733936a..db4374cf3e 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -564,7 +564,7 @@ partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLi
                  Example: suppose we have
                    `?m t1 t2 t3`
                  That is, `f := ?m` and `args := #[t1, t2, t3]`
-                 Morever, `?m` is delayed assigned
+                 Moreover, `?m` is delayed assigned
                    `?m #[x, y] := f x y`
                  where, `fvars := #[x, y]` and `newVal := f x y`.
                  After abstracting `newVal`, we have `f (Expr.bvar 0) (Expr.bvar 1)`.
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 02c950885c..d34063e055 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1183,7 +1183,7 @@ def runLongestMatchParser (left? : Option Syntax) (startLhsPrec : Nat) (p : Pars
     -- error with an unexpected number of nodes.
     s.shrinkStack startSize |>.pushSyntax Syntax.missing
   else
-    -- parser succeded with incorrect number of nodes
+    -- parser succeeded with incorrect number of nodes
     invalidLongestMatchParser s
 
 def longestMatchStep (left? : Option Syntax) (startSize startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (prio : Nat) (p : ParserFn)
@@ -1715,8 +1715,8 @@ partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) (s :
   After processing the leading parser, we chain with parsers from `trailingTable`/`trailingParsers` that have precedence
   at least `c.prec` where `c` is the `ParsingContext`. Recall that `c.prec` is set by `categoryParser`.
 
-  Note that in the original Pratt's algorith, precedences are only checked before calling trailing parsers. In our
-  implementation, leading *and* trailing parsers check the precendece. We claim our algorithm is more flexible,
+  Note that in the original Pratt's algorithm, precedences are only checked before calling trailing parsers. In our
+  implementation, leading *and* trailing parsers check the precedence. We claim our algorithm is more flexible,
   modular and easier to understand.
 
   `antiquotParser` should be a `mkAntiquot` parser (or always fail) and is tried before all other parsers.
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index 00fb6c747a..b5ae3360ab 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -55,7 +55,7 @@ def getRevAliases (env : Environment) (e : Name) : List Name :=
 /-! # Global name resolution -/
 namespace ResolveName
 
-/-- Check whether `ns ++ id` is a valid namepace name and/or there are aliases names `ns ++ id`. -/
+/-- Check whether `ns ++ id` is a valid namespace name and/or there are aliases names `ns ++ id`. -/
 private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name :=
   let resolvedId    := ns ++ id
   -- We ignore protected aliases if `id` is atomic.
@@ -160,7 +160,7 @@ Given a name `id` try to find namespaces it may refer to. The resolution procedu
    then we include `s_1 . ... . s_i ++ n` in the result if it is the name of an existing namespace.
    We search "backwards", and include at most one of the in the list of resulting namespaces.
 
-2- If `id` is the extact name of an existing namespace, then include `id`
+2- If `id` is the exact name of an existing namespace, then include `id`
 
 3- Finally, for each command `open N`, include in the result `N ++ n` if it is the name of an existing namespace.
    We only consider simple `open` commands. -/
@@ -253,7 +253,7 @@ def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m]
   | _   => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}"
 
 /-- Interpret the syntax `n` as an identifier for a global constant, and return a list of resolved
-constant names that it could be refering to based on the currently open namespaces.
+constant names that it could be referring to based on the currently open namespaces.
 This should be used instead of `resolveGlobalConstCore` for identifiers taken from syntax
 because `Syntax` objects may have names that have already been resolved.
 
diff --git a/src/Lean/Server/AsyncList.lean b/src/Lean/Server/AsyncList.lean
index ef64d7322d..5da2648899 100644
--- a/src/Lean/Server/AsyncList.lean
+++ b/src/Lean/Server/AsyncList.lean
@@ -83,7 +83,7 @@ partial def waitUntil (p : α → Bool) : AsyncList ε α → Task (List α × O
 def waitAll : AsyncList ε α → Task (List α × Option ε) :=
   waitUntil (fun _ => false)
 
-/-- Spawns a `Task` acting like `List.find?` but which will wait for tail evalution
+/-- Spawns a `Task` acting like `List.find?` but which will wait for tail evaluation
 when necessary to traverse the list. If the tail terminates before a matching element
 is found, the task throws the terminating value. -/
 partial def waitFind? (p : α → Bool) : AsyncList ε α → Task (Except ε (Option α))
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 4c3ef01d83..99815d87da 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -38,13 +38,13 @@ File processing and requests+notifications against a file should be concurrent f
 
 To achieve these goals, elaboration is executed in a chain of tasks, where each task corresponds to
 the elaboration of one command. When the elaboration of one command is done, the next task is spawned.
-On didChange notifications, we search for the task in which the change occured. If we stumble across
+On didChange notifications, we search for the task in which the change occurred. If we stumble across
 a task that has not yet finished before finding the task we're looking for, we terminate it
-and start the elaboration there, otherwise we start the elaboration at the task where the change occured.
+and start the elaboration there, otherwise we start the elaboration at the task where the change occurred.
 
 Requests iterate over tasks until they find the command that they need to answer the request.
 In order to not block the main thread, this is done in a request task.
-If a task that the request task waits for is terminated, a change occured somewhere before the
+If a task that the request task waits for is terminated, a change occurred somewhere before the
 command that the request is looking for and the request sends a "content changed" error.
 -/
 
@@ -104,7 +104,7 @@ section Elab
     -- TODO(MH): check for interrupt with increased precision
     cancelTk.check
     /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
-      while prefering newer versions over old ones. The former is necessary because we do
+      while preferring newer versions over old ones. The former is necessary because we do
       not explicitly clear older diagnostics, while the latter is necessary because we do
       not guarantee that diagnostics are emitted in order. Specifically, it may happen that
       we interrupted this elaboration task right at this point and a newer elaboration task
@@ -112,7 +112,7 @@ section Elab
       the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
       because we cannot guarantee that no further diagnostics are emitted after clearing
       them. -/
-    -- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot
+    -- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
     -- because empty diagnostics clear existing error/information squiggles. Therefore we always
     -- want to publish in case there was previously a message at this position.
     publishDiagnostics m snap.diagnostics.toArray ctx.hOut
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index a9f52e2472..bd0196f2bd 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -24,7 +24,7 @@ functionality is purpose-specific to showing the contents of infoview popups.
 For use in standard LSP go-to-definition (see `Lean.Server.FileWorker.locationLinksOfInfo`),
 all the elaborator information we need for similar tasks is already fully recoverable via
 the `InfoTree` structure (see `Lean.Elab.InfoTree.visitM`).
-There we use this as a convienience wrapper for queried nodes (e.g. the return value of
+There we use this as a convenience wrapper for queried nodes (e.g. the return value of
 `Lean.Elab.InfoTree.hoverableInfoAt?`). It also includes the children info nodes
 as additional context (this is unused in the RPC case, as delaboration has no notion of child nodes).
 
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index b67bb04ddb..4c4707d033 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -105,7 +105,7 @@ section FileWorker
     -- This should not be mutated outside of namespace FileWorker, as it is used as shared mutable state
     /-- The pending requests map contains all requests
     that have been received from the LSP client, but were not answered yet.
-    We need them for forwaring cancellation requests to the correct worker as well as cleanly aborting
+    We need them for forwarding cancellation requests to the correct worker as well as cleanly aborting
     requests on worker crashes. -/
     pendingRequestsRef : IO.Ref PendingRequestMap
 
diff --git a/src/Lean/Util/OccursCheck.lean b/src/Lean/Util/OccursCheck.lean
index d6b3326484..90f982d043 100644
--- a/src/Lean/Util/OccursCheck.lean
+++ b/src/Lean/Util/OccursCheck.lean
@@ -9,7 +9,7 @@ namespace Lean
 
 /--
   Return true if `e` does **not** contain `mvarId` directly or indirectly
-  This function considers assigments and delayed assignments. -/
+  This function considers assignments and delayed assignments. -/
 partial def occursCheck [Monad m] [MonadMCtx m] (mvarId : MVarId) (e : Expr) : m Bool := do
   if !e.hasExprMVar then
     return true
diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out
index 2a3987f5fc..c6094eae6f 100644
--- a/tests/lean/docStr.lean.expected.out
+++ b/tests/lean/docStr.lean.expected.out
@@ -17,7 +17,7 @@ doc string for 'g' is not available
 "let rec documentation at g "
 "Gadget for optional parameter support.\n\nA binder like `(x : α := default)` in a declaration is syntax sugar for\n`x : optParam α default`, and triggers the elaborator to attempt to use\n`default` to supply the argument if it is not supplied.\n"
 "Auxiliary declaration used to implement named patterns like `x@h:p`. "
-"Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues bulding the telescope if it is a `forall`. "
+"Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues building the telescope if it is a `forall`. "
 Foo :=
   { range := { pos := { line := 4, column := 0 },
                charUtf16 := 0,