chore: fix spelling mistakes in src/Lean/Elab/ (#5435)

Co-authored-by: euprunin <[email protected]>

src/Lean/Elab/AuxDef.lean

@@ -24,7 +24,7 @@ def elabAuxDef : CommandElab
     let id := `_aux ++ (← getMainModule) ++ `_ ++ id
     let id := String.intercalate "_" <| id.components.map (·.toString (escape := false))
     let ns ← getCurrNamespace
-    -- make sure we only add a single component so that scoped workes
+    -- make sure we only add a single component so that scoped works
     let id ← mkAuxName (ns.mkStr id) 1
     let id := id.replacePrefix ns Name.anonymous -- TODO: replace with def _root_.id
     elabCommand <|

src/Lean/Elab/Binders.lean

@@ -650,7 +650,7 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
     /-
     We use `withSynthesize` to ensure that any postponed elaboration problem
     and nested tactics in `type` are resolved before elaborating `val`.
-    Resolved: we want to avoid synthethic opaque metavariables in `type`.
+    Resolved: we want to avoid synthetic opaque metavariables in `type`.
     Recall that this kind of metavariable is non-assignable, and `isDefEq`
     may waste a lot of time unfolding declarations before failing.
     See issue #4051 for an example.

src/Lean/Elab/BuiltinCommand.lean

@@ -381,7 +381,7 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax): CommandElabM Uni
     -- Evaluate using term using `MetaEval` class.
     let elabMetaEval : CommandElabM Unit := do
       -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
-      -- we don't polute the environment with auxliary declarations.
+      -- we don't pollute the environment with auxliary declarations.
       -- We have special support for `CommandElabM` to ensure `#eval` can be used to execute commands
       -- that modify `CommandElabM` state not just the `Environment`.
       let act : Sum (CommandElabM Unit) (Environment → Options → IO (String × Except IO.Error Environment)) ←

src/Lean/Elab/DeclModifiers.lean

@@ -120,7 +120,7 @@ section Methods
 
 variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m]
 
-/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `proctected`, `unsafe`, `noncomputable`, doc string)-/
+/-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/
 def elabModifiers (stx : Syntax) : m Modifiers := do
   let docCommentStx := stx[0]
   let attrsStx      := stx[1]

src/Lean/Elab/Extra.lean

@@ -375,7 +375,7 @@ private def hasHeterogeneousDefaultInstances (f : Expr) (maxType : Expr) (lhs :
   return false
 
 /--
-  Return `true` if polymorphic function `f` has a homogenous instance of `maxType`.
+  Return `true` if polymorphic function `f` has a homogeneous instance of `maxType`.
   The coercions to `maxType` only makes sense if such instance exists.
 
   For example, suppose `maxType` is `Int`, and `f` is `HPow.hPow`. Then,
@@ -421,9 +421,9 @@ mutual
       | .binop ref kind f lhs rhs =>
         /-
           We only keep applying coercions to `maxType` if `f` is predicate or
-          `f` has a homogenous instance with `maxType`. See `hasHomogeneousInstance` for additional details.
+          `f` has a homogeneous instance with `maxType`. See `hasHomogeneousInstance` for additional details.
 
-          Remark: We assume `binrel%` elaborator is only used with homogenous predicates.
+          Remark: We assume `binrel%` elaborator is only used with homogeneous predicates.
         -/
         if (← pure isPred <||> hasHomogeneousInstance f maxType) then
           return .binop ref kind f (← go lhs f true false) (← go rhs f false false)

src/Lean/Elab/Match.lean

@@ -30,7 +30,7 @@ private def mkUserNameFor (e : Expr) : TermElabM Name := do
 
 
 /--
-   Remark: if the discriminat is `Systax.missing`, we abort the elaboration of the `match`-expression.
+   Remark: if the discriminat is `Syntax.missing`, we abort the elaboration of the `match`-expression.
    This can happen due to error recovery. Example
    ```
    example : (p ∨ p) → p := fun h => match

src/Lean/Elab/PreDefinition/Main.lean

@@ -104,7 +104,7 @@ Checks consistency of a clique of TerminationHints:
 
 * If not all have a hint, the hints are ignored (log error)
 * If one has `structural`, check that all have it, (else throw error)
-* A `structural` shold not have a `decreasing_by` (else log error)
+* A `structural` should not have a `decreasing_by` (else log error)
 
 -/
 def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -119,7 +119,7 @@ def getRecArgInfos (fnName : Name) (xs : Array Expr) (value : Expr)
     (termArg? : Option TerminationArgument) : MetaM (Array RecArgInfo × MessageData) := do
   lambdaTelescope value fun ys _ => do
     if let .some termArg := termArg? then
-      -- User explictly asked to use a certain argument, so throw errors eagerly
+      -- User explicitly asked to use a certain argument, so throw errors eagerly
       let recArgInfo ← withRef termArg.ref do
         mapError (f := (m!"cannot use specified parameter for structural recursion:{indentD ·}")) do
           getRecArgInfo fnName xs.size (xs ++ ys) (← termArg.structuralArg)
@@ -189,7 +189,7 @@ def argsInGroup (group : IndGroupInst) (xs : Array Expr) (value : Expr)
     if (← group.isDefEq recArgInfo.indGroupInst) then
       return (.some recArgInfo)
 
-    -- Can this argument be understood as the auxillary type former of a nested inductive?
+    -- Can this argument be understood as the auxiliary type former of a nested inductive?
     if nestedTypeFormers.isEmpty then return .none
     lambdaTelescope value fun ys _ => do
       let x := (xs++ys)[recArgInfo.recArgPos]!

src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean

@@ -13,7 +13,7 @@ This module contains the types
 * `IndGroupInst` which extends `IndGroupInfo` with levels and parameters
    to indicate a instantiation of the group.
 
-One purpose of this abstraction is to make it clear when a fuction operates on a group as
+One purpose of this abstraction is to make it clear when a function operates on a group as
 a whole, rather than a specific inductive within the group.
 -/
 

src/Lean/Elab/PreDefinition/Structural/Preprocess.lean

@@ -17,7 +17,7 @@ private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool :=
     false
 
 /--
-Preprocesses the expessions to improve the effectiveness of `elimRecursion`.
+Preprocesses the expressions to improve the effectiveness of `elimRecursion`.
 
 * Beta reduce terms where the recursive function occurs in the lambda term.
   Example:

src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean

@@ -31,7 +31,7 @@ structure RecArgInfo where
   indGroupInst : IndGroupInst
   /--
   index of the inductive datatype of the argument we are recursing on.
-  If `< indAll.all`, a normal data type, else an auxillary data type due to nested recursion
+  If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion
   -/
   indIdx       : Nat
 deriving Inhabited
@@ -52,7 +52,7 @@ def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array E
   return (indexMajorArgs, otherArgs)
 
 /--
-Name of the recursive data type. Assumes that it is not one of the auxillary ones.
+Name of the recursive data type. Assumes that it is not one of the auxiliary ones.
 -/
 def RecArgInfo.indName! (info : RecArgInfo) : Name :=
   info.indGroupInst.all[info.indIdx]!

src/Lean/Elab/PreDefinition/TerminationArgument.lean

@@ -112,7 +112,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
       let stxBody ← Delaborator.delab
       let hole : TSyntax `Lean.Parser.Term.hole ← `(hole|_)
 
-      -- any variable not mentioned syntatically (it may appear in the `Expr`, so do not just use
+      -- any variable not mentioned syntactically (it may appear in the `Expr`, so do not just use
       -- `e.bindingBody!.hasLooseBVar`) should be delaborated as a hole.
       let vars  : TSyntaxArray [`ident, `Lean.Parser.Term.hole] :=
         Array.map (fun (i : Ident) => if stxBody.raw.hasIdent i.getId then i else hole) vars

src/Lean/Elab/PreDefinition/TerminationHint.lean

@@ -45,7 +45,7 @@ structure TerminationHints where
   decreasingBy?  : Option DecreasingBy
   /--
   Here we record the number of parameters past the `:`. It is set by
-  `TerminationHints.rememberExtraParams` and used as folows:
+  `TerminationHints.rememberExtraParams` and used as follows:
 
   * When we guess the termination argument in `GuessLex` and want to print it in surface-syntax
     compatible form.

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -66,7 +66,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
           else if let some mvarIds ← splitTarget? mvarId then
             mvarIds.forM go
           else
-            -- At some point in the past, we looked for occurences of Wf.fix to fold on the
+            -- At some point in the past, we looked for occurrences of Wf.fix to fold on the
             -- LHS (introduced in 096e4eb), but it seems that code path was never used,
             -- so #3133 removed it again (and can be recovered from there if this was premature).
             throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -29,7 +29,7 @@ if given, or the default `decreasing_tactic`.
 
 For mutual recursion, a single measure is not just one parameter, but one from each recursive
 function. Enumerating these can lead to a combinatoric explosion, so we bound
-the nubmer of measures tried.
+the number of measures tried.
 
 In addition to measures derived from `sizeOf xᵢ`, it also considers measures
 that assign an order to the functions themselves. This way we can support mutual
@@ -42,7 +42,7 @@ guessed lexicographic order.
 
 The following optimizations are applied to make this feasible:
 
-1. The crucial optimiziation is to look at each argument of each recursive call
+1. The crucial optimization is to look at each argument of each recursive call
    _once_, try to prove `<` and (if that fails `≤`), and then look at that table to
    pick a suitable measure.
 
@@ -80,7 +80,7 @@ register_builtin_option showInferredTerminationBy : Bool := {
 
 
 /--
-Given a predefinition, return the variabe names in the outermost lambdas.
+Given a predefinition, return the variable names in the outermost lambdas.
 Includes the “fixed prefix”.
 
 The length of the returned array is also used to determine the arity
@@ -550,7 +550,7 @@ where
         failure
 
 /--
-Enumerate all meausures we want to try.
+Enumerate all measures we want to try.
 
 All arguments (resp. combinations thereof) and
 possible orderings of functions (if more than one)

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

@@ -17,7 +17,7 @@ private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool :=
     false
 
 /--
-Preprocesses the expessions to improve the effectiveness of `wfRecursion`.
+Preprocesses the expressions to improve the effectiveness of `wfRecursion`.
 
 * Floats out the RecApp markers.
   Example:

src/Lean/Elab/RecAppSyntax.lean

@@ -29,7 +29,7 @@ def getRecAppSyntax? (e : Expr) : Option Syntax :=
   | _                => none
 
 /--
-Checks if the `MData` is for a recursive applciation.
+Checks if the `MData` is for a recursive application.
 -/
 def MData.isRecApp (d : MData) : Bool :=
   d.contains recAppKey

src/Lean/Elab/SyntheticMVars.lean

@@ -21,7 +21,7 @@ private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSo
     elabTerm stx expectedType? false
 
 /--
-  Try to elaborate `stx` that was postponed by an elaboration method using `Expection.postpone`.
+  Try to elaborate `stx` that was postponed by an elaboration method using `Exception.postpone`.
   It returns `true` if it succeeded, and `false` otherwise.
   It is used to implement `synthesizeSyntheticMVars`. -/
 private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId : MVarId) (postponeOnError : Bool) : TermElabM Bool :=
@@ -86,7 +86,7 @@ private def synthesizePendingInstMVar (instMVar : MVarId) (extraErrorMsg? : Opti
   example (a : Int) (b c : Nat) : a = ↑b - ↑c := sorry
   ```
   We have two pending coercions for the `↑` and `HSub ?m.220 ?m.221 ?m.222`.
-  When we did not use a backtracking search here, then the homogenous default instance for `HSub`.
+  When we did not use a backtracking search here, then the homogeneous default instance for `HSub`.
   ```
   instance [Sub α] : HSub α α α where
   ```
@@ -306,7 +306,7 @@ inductive PostponeBehavior where
   | no
   /--
   Synthectic metavariables associated with type class resolution can be postponed.
-  Motivation: this kind of metavariable are not synthethic opaque, and can be assigned by `isDefEq`.
+  Motivation: this kind of metavariable are not synthetic opaque, and can be assigned by `isDefEq`.
   Unviverse constraints can also be postponed.
   -/
   | «partial»

src/Lean/Elab/Tactic/BVDecide.lean

@@ -71,7 +71,7 @@ For the second kind more steps are involved:
 3. Verify that algorithm in `Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas`.
 4. Integrate it with either the expression or predicate bitblaster and use the proof above to verify it.
 5. Add simplification lemmas for the primitive to `bv_normalize` in `Std.Tactic.BVDecide.Normalize`.
-   If there are mutliple ways to write the primitive (e.g. with TC based notation and without) you
+   If there are multiple ways to write the primitive (e.g. with TC based notation and without) you
    should normalize for one notation here.
 6. Add the reflection code to `Lean.Elab.Tactic.BVDecide.Frontend.BVDecide`
 7. Add a test!

src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean

@@ -24,7 +24,7 @@ register_builtin_option sat.solver : String := {
   defValue := ""
   descr :=
     "Name of the SAT solver used by Lean.Elab.Tactic.BVDecide tactics.\n
-     1. If this is set to something besides the emtpy string they will use that binary.\n
+     1. If this is set to something besides the empty string they will use that binary.\n
      2. If this is set to the empty string they will check if there is a cadical binary next to the\
         executing program. Usually that program is going to be `lean` itself and we do ship a\
         `cadical` next to it.\n

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -270,7 +270,7 @@ structure Result where
   -/
   simpTrace : Simp.Stats
   /--
-  If the normalization step was not enough to solve the goal this contaisn the LRAT proof
+  If the normalization step was not enough to solve the goal this contains the LRAT proof
   certificate.
   -/
   lratCert : Option LratCert

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -77,7 +77,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
 
 -- mvarIds is the list of goals produced by congr. We only want to change the one at position `i`
 -- so this closes all other equality goals with `rfl.`. There are non-equality goals produced
--- by `congr` (e.g. dependent instances), thes are kept as goals.
+-- by `congr` (e.g. dependent instances), these are kept as goals.
 private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) :
   TacticM Unit := do
   if i >= 0 then

src/Lean/Elab/Tactic/Omega.lean

@@ -39,7 +39,7 @@ The `omega` tactic pre-processes the hypotheses in the following ways:
 * If `x / m` appears, for some `x : Int` and literal `m : Nat`,
   replace `x / m` with a new variable `α` and add the constraints
   `0 ≤ - m * α + x ≤ m - 1`.
-* If `x % m` appears, similarly, introduce the same new contraints
+* If `x % m` appears, similarly, introduce the same new constraints
   but replace `x % m` with `- m * α + x`.
 * Split conjunctions, existentials, and subtypes.
 * Record, for each appearance of `(a - b : Int)` with `a b : Nat`, the disjunction

src/Lean/Elab/Tactic/Omega/Core.lean

@@ -49,7 +49,7 @@ inductive Justification : Constraint → Coeffs → Type
   | combo {s t x y} (a : Int) (j : Justification s x) (b : Int) (k : Justification t y) :
     Justification (Constraint.combo a s b t) (Coeffs.combo a x b y)
   /--
-  The justification for the constraing constructed using "balanced mod" while
+  The justification for the constraint constructed using "balanced mod" while
   eliminating an equality.
   -/
   | bmod (m : Nat) (r : Int) (i : Nat) {x} (j : Justification (.exact r) x) :

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -322,7 +322,7 @@ where
 end
 namespace MetaProblem
 
-/-- The trivial `MetaProblem`, with no facts to processs and a trivial `Problem`. -/
+/-- The trivial `MetaProblem`, with no facts to process and a trivial `Problem`. -/
 def trivial : MetaProblem where
   problem := {}
 

src/Lean/Elab/Term.lean

@@ -1045,7 +1045,7 @@ def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM
   logException ex
   pure syntheticSorry
 
-/-- If `mayPostpone == true`, throw `Expection.postpone`. -/
+/-- If `mayPostpone == true`, throw `Exception.postpone`. -/
 def tryPostpone : TermElabM Unit := do
   if (← read).mayPostpone then
     throwPostpone