chore: fix typos in comments

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

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

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

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

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

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.
 -/

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

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

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
 
 /--

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 :=

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

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

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.
 ```

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

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

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:
 ```

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`.
 

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}

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
     /-

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

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

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`

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:
                  -----------------------------------------------------------

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)

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
      ```

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

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.
 -/

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.
 -/

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 := #[]
   /--

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

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

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
 

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)+)
 ```

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) }

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

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

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!

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)
 

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

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

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

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)`

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.
   -/

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)

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

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.

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

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.
 -/

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

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)

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 :=

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

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

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`.
 

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 =>

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

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 :=

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

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₂) :

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

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`.
 -/

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

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)`.

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.

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.
 

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 α))

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

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).
 

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
 

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

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,