diff --git a/doc/dev/bootstrap.md b/doc/dev/bootstrap.md
index 554c39a308..12f84edea4 100644
--- a/doc/dev/bootstrap.md
+++ b/doc/dev/bootstrap.md
@@ -73,7 +73,7 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
 The github repository will automatically update stage0 on `master` once
 `src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
 
-If you have write access to the lean4 repository, you can also also manually
+If you have write access to the lean4 repository, you can also manually
 trigger that process, for example to be able to use new features in the compiler itself.
 You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
 or using Github CLI with
diff --git a/doc/examples/tc.lean b/doc/examples/tc.lean
index 56bc18cf4f..c6c3cd21a7 100644
--- a/doc/examples/tc.lean
+++ b/doc/examples/tc.lean
@@ -29,7 +29,7 @@ inductive HasType : Expr → Ty → Prop
 
 /-!
 We can easily show that if `e` has type `t₁` and type `t₂`, then `t₁` and `t₂` must be equal
-by using the the `cases` tactic. This tactic creates a new subgoal for every constructor,
+by using the `cases` tactic. This tactic creates a new subgoal for every constructor,
 and automatically discharges unreachable cases. The tactic combinator `tac₁ <;> tac₂` applies
 `tac₂` to each subgoal produced by `tac₁`. Then, the tactic `rfl` is used to close all produced
 goals using reflexivity.
@@ -82,7 +82,7 @@ theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .un
 /-!
 Now, we prove that if `Expr.typeCheck e` returns `Maybe.unknown`, then forall `ty`, `HasType e ty` does not hold.
 The notation `e.typeCheck` is sugar for `Expr.typeCheck e`. Lean can infer this because we explicitly said that `e` has type `Expr`.
-The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to to rename "inaccessible" variables.
+The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to rename "inaccessible" variables.
 We say a variable is inaccessible if it is introduced by a tactic (e.g., `cases`) or has been shadowed by another variable introduced
 by the user. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes
 the cases corresponding to the constructors `Expr.nat` and `Expr.bool`.
diff --git a/doc/expressions.md b/doc/expressions.md
index e042dff40d..b8a9bb8910 100644
--- a/doc/expressions.md
+++ b/doc/expressions.md
@@ -396,7 +396,7 @@ Every expression in Lean has a natural computational interpretation, unless it i
 
 * *β-reduction* : An expression ``(λ x, t) s`` β-reduces to ``t[s/x]``, that is, the result of replacing ``x`` by ``s`` in ``t``.
 * *ζ-reduction* : An expression ``let x := s in t`` ζ-reduces to ``t[s/x]``.
-* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to to ``t``.
+* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to ``t``.
 * *ι-reduction* : When a function defined by recursion on an inductive type is applied to an element given by an explicit constructor, the result ι-reduces to the specified function value, as described in [Inductive Types](inductive.md).
 
 The reduction relation is transitive, which is to say, is ``s`` reduces to ``s'`` and ``t`` reduces to ``t'``, then ``s t`` reduces to ``s' t'``, ``λ x, s`` reduces to ``λ x, s'``, and so on. If ``s`` and ``t`` reduce to a common term, they are said to be *definitionally equal*. Definitional equality is defined to be the smallest equivalence relation that satisfies all these properties and also includes α-equivalence and the following two relations:
diff --git a/doc/monads/laws.lean b/doc/monads/laws.lean
index cbcef0b134..bef495a1c3 100644
--- a/doc/monads/laws.lean
+++ b/doc/monads/laws.lean
@@ -171,7 +171,7 @@ of data contained in the container resulting in a new container that has the sam
 
 `u <*> pure y = pure (. y) <*> u`.
 
-This law is is a little more complicated, so don't sweat it too much. It states that the order that
+This law is a little more complicated, so don't sweat it too much. It states that the order that
 you wrap things shouldn't matter. One the left, you apply any applicative `u` over a pure wrapped
 object. On the right, you first wrap a function applying the object as an argument. Note that `(·
 y)` is short hand for: `fun f => f y`. Then you apply this to the first applicative `u`. These
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 41ce76ed4d..6492317449 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -862,7 +862,7 @@ partial def decodeRawStrLitAux (s : String) (i : String.Pos) (num : Nat) : Strin
 /--
 Takes the string literal lexical syntax parsed by the parser and interprets it as a string.
 This is where escape sequences are processed for example.
-The string `s` is is either a plain string literal or a raw string literal.
+The string `s` is either a plain string literal or a raw string literal.
 
 If it returns `none` then the string literal is ill-formed, which indicates a bug in the parser.
 The function is not required to return `none` if the string literal is ill-formed.
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index d5f7727330..57ed1572df 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -456,7 +456,7 @@ syntax (name := change) "change " term (location)? : tactic
 
 /--
 * `change a with b` will change occurrences of `a` to `b` in the goal,
-  assuming `a` and `b` are are definitionally equal.
+  assuming `a` and `b` are definitionally equal.
 * `change a with b at h` similarly changes `a` to `b` in the type of hypothesis `h`.
 -/
 syntax (name := changeWith) "change " term " with " term (location)? : tactic
diff --git a/src/Lean/Compiler/LCNF/JoinPoints.lean b/src/Lean/Compiler/LCNF/JoinPoints.lean
index b92b80750b..f92f81b040 100644
--- a/src/Lean/Compiler/LCNF/JoinPoints.lean
+++ b/src/Lean/Compiler/LCNF/JoinPoints.lean
@@ -242,7 +242,7 @@ structure ExtendState where
   /--
   A map from join point `FVarId`s to a respective map from free variables
   to `Param`s. The free variables in this map are the once that the context
-  of said join point will be extended by by passing in the respective parameter.
+  of said join point will be extended by passing in the respective parameter.
   -/
   fvarMap : Std.HashMap FVarId (Std.HashMap FVarId Param) := {}
 
diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
index 609cd975fc..d3aaedd122 100644
--- a/src/Lean/Data/HashMap.lean
+++ b/src/Lean/Data/HashMap.lean
@@ -195,7 +195,7 @@ def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
 
 /--
 Similar to `insert`, but returns `some old` if the map already had an entry `α → old`.
-If the result is `some old`, the the resulting map is equal to `m`. -/
+If the result is `some old`, the resulting map is equal to `m`. -/
 def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option β :=
   match m with
   | ⟨ m, hw ⟩ =>
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 7e2ae65993..38372ebae9 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -18,7 +18,7 @@ private def getMonadForIn (expectedType? : Option Expr) : TermElabM Expr := do
     | some expectedType =>
       match (← isTypeApp? expectedType) with
       | some (m, _) => return m
-      | none => throwError "invalid 'for_in%' notation, expected type is not of of the form `M α`{indentExpr expectedType}"
+      | none => throwError "invalid 'for_in%' notation, expected type is not of the form `M α`{indentExpr expectedType}"
 
 private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
   throwError "failed to synthesize instance for 'for_in%' notation{indentExpr forInInstance}"
diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index 4bb591844f..6c348d1561 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -269,7 +269,7 @@ def inferBRecOnFTypes (recArgInfos : Array RecArgInfo) (positions : Positions)
   let brecOnType ← inferType brecOn
   -- Skip the indices and major argument
   let packedFTypes ← forallBoundedTelescope brecOnType (some (recArgInfo.indicesPos.size + 1)) fun _ brecOnType =>
-    -- And return the types of of the next arguments
+    -- And return the types of the next arguments
     arrowDomainsN numTypeFormers brecOnType
 
   let mut FTypes := Array.mkArray positions.numIndices (Expr.sort 0)
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 61691c007a..d67bfd8d14 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -605,7 +605,7 @@ private partial def hasNoErrorIfUnused : Syntax → Bool
 
 /--
 Given `rhss` the right-hand-sides of a `match`-syntax notation,
-We tag them with with fresh identifiers `alt_idx`. We use them to detect whether an alternative
+We tag them with fresh identifiers `alt_idx`. We use them to detect whether an alternative
 has been used or not.
 The result is a triple `(altIdxMap, ignoreIfUnused, rhssNew)` where
 - `altIdxMap` is a mapping from the `alt_idx` identifiers to right-hand-side indices.
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 1eb1152448..a5378133af 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -512,7 +512,7 @@ private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α :=
   finally
     modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
 
-/-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use use `synthesizeUsingDefault` -/
+/-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use `synthesizeUsingDefault` -/
 @[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] (k : m α) : m α :=
   monadMap (m := TermElabM) (withSynthesizeLightImp ·) k
 
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index e8ead0767e..9a7a723fee 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -451,7 +451,7 @@ modify it, use `PersistentEnvExtension.addEntry`, with an `addEntryFn` that perf
 modification.
 
 When a module is loaded, the values saved by all of its dependencies for this
-`PersistentEnvExtension` are are available as an `Array (Array α)` via the environment extension,
+`PersistentEnvExtension` are available as an `Array (Array α)` via the environment extension,
 with one array per transitively imported module. The state of type `σ` used in the current module
 can be initialized from these imports by specifying a suitable `addImportedFn`. The `addImportedFn`
 runs at the beginning of elaboration for every module, so it's usually better for performance to
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index edc0c6aa23..111c4e17f0 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -420,7 +420,7 @@ def indentExpr (e : Expr) : MessageData :=
 
 class AddMessageContext (m : Type → Type) where
   /--
-  Without context, a `MessageData` object may be be missing information
+  Without context, a `MessageData` object may be missing information
   (e.g. hover info) for pretty printing, or may print an error. Hence,
   `addMessageContext` should be called on all constructed `MessageData`
   (e.g. via `m!`) before taking it out of context (e.g. leaving `MetaM` or
diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean
index baf8095401..8c1b8e7752 100644
--- a/src/Lean/Meta/ArgsPacker.lean
+++ b/src/Lean/Meta/ArgsPacker.lean
@@ -64,7 +64,7 @@ def packType (xs : Array Expr) : MetaM Expr := do
 
 /--
 Create a unary application by packing the given arguments using `PSigma.mk`.
-The `type` should be the the expected type of the packed argument, as created with `packType`.
+The `type` should be the expected type of the packed argument, as created with `packType`.
 -/
 partial def pack (type : Expr) (args : Array Expr) : Expr := go 0 type
 where
diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean
index ddc2a64e1b..f076c6a1ce 100644
--- a/src/Lean/Meta/CongrTheorems.lean
+++ b/src/Lean/Meta/CongrTheorems.lean
@@ -319,7 +319,7 @@ where
 /--
 Create a congruence theorem for `f`. The theorem is used in the simplifier.
 
-If `subsingletonInstImplicitRhs = true`, the the `rhs` corresponding to `[Decidable p]` parameters
+If `subsingletonInstImplicitRhs = true`, the `rhs` corresponding to `[Decidable p]` parameters
 is marked as instance implicit. It forces the simplifier to compute the new instance when applying
 the congruence theorem.
 For the `congr` tactic we set it to `false`.
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index c3bf86ceb4..cf5a576f14 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -28,7 +28,7 @@ register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
   This function is used to filter unification problems in
   `isDefEqArgs`/`isDefEqEtaStruct` where we can assign proofs.
   If one side is of the form described above, then we can likely assign `?m`.
-  But it it's not, we would most likely apply proof irrelevance, which is
+  But if it's not, we would most likely apply proof irrelevance, which is
   usually very expensive since it needs to unify the types as well.
 -/
 def isAbstractedUnassignedMVar : Expr → MetaM Bool
@@ -978,7 +978,7 @@ where
   occursCheck (type : Expr) : Bool :=
     let go : StateM MetavarContext Bool := do
       Lean.occursCheck mvarId type
-    -- Remark: it is ok to discard the the "updated" `MetavarContext` because
+    -- Remark: it is ok to discard the "updated" `MetavarContext` because
     -- this function assumes all assigned metavariables have already been
     -- instantiated.
     go.run' mctx
@@ -1486,7 +1486,7 @@ private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : Meta
   ```
   Foo.pow x 256 =?= Pow.pow x 256
   ```
-  where the the `Pow` instance is wrapping `Foo.pow`
+  where the `Pow` instance is wrapping `Foo.pow`
   See issue #1419 for the complete example.
 -/
 private partial def unfoldNonProjFnDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool := do
diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean
index e339f6a4cc..556f33d6d2 100644
--- a/src/Lean/Meta/Match/MatcherApp/Transform.lean
+++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean
@@ -49,7 +49,7 @@ private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNu
   - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size`
   - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]`
 
-  This is used in in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to
+  This is used in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to
   the argument provided by `fix` to refine the termination argument, which may mention `major`.
   See there for how to use this function.
 -/
@@ -108,7 +108,7 @@ def addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option MatcherApp) :=
   This is similar to `MatcherApp.addArg` when you only have an expression to
   refined, and not a type with a value.
 
-  This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive
+  This is used in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive
   calls to refine the functions' parameter, which may mention `major`.
   See there for how to use this function.
 -/
@@ -202,7 +202,7 @@ NB: Not all operations on `MatcherApp` can handle one `matcherName` is a splitte
 If `addEqualities` is true, then equalities connecting the discriminant to the parameters of the
 alternative (like in `match h : x with …`) are be added, if not already there.
 
-This function works even if the the type of alternatives do *not* fit the inferred type. This
+This function works even if the type of alternatives do *not* fit the inferred type. This
 allows you to post-process the `MatcherApp` with `MatcherApp.inferMatchType`, which will
 infer a type, given all the alternatives.
 -/
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 166fe8f493..b2d077115e 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -51,7 +51,7 @@ Here "branch" roughly corresponds to tail-call positions: branches of top-level
 For every recursive call in that branch, an induction hypothesis asserting the
 motive for the arguments of the recursive call is provided.
 If the recursive call is under binders and it, or its proof of termination,
-depend on the the bound values, then these become assumptions of the inductive
+depend on the bound values, then these become assumptions of the inductive
 hypothesis.
 
 Additionally, the local context of the branch (e.g. the condition of an
@@ -703,7 +703,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
         let e' ← mkLambdaFVars #[motive] e'
 
         -- We could pass (usedOnly := true) below, and get nicer induction principles that
-        -- do do not mention odd unused parameters.
+        -- do not mention odd unused parameters.
         -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
         -- that derives them from an function application in the goal) is harder, as
         -- one would have to infer or keep track of which parameters to pass.
@@ -918,7 +918,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
       unless brecOnTargets.all (·.isFVar) do
         throwError "the indices and major argument of the brecOn application are not variables:{indentExpr body}"
       unless brecOnExtras.all (·.isFVar) do
-        throwError "the extra arguments to the the brecOn application are not variables:{indentExpr body}"
+        throwError "the extra arguments to the brecOn application are not variables:{indentExpr body}"
       let lvl :: indLevels := us |throwError "Too few universe parameters in .brecOn application:{indentExpr body}"
 
       let group : Structural.IndGroupInst := { Structural.IndGroupInfo.ofInductiveVal indInfo with
@@ -1041,7 +1041,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
           let e' ← mkLambdaFVars motives e'
 
           -- We could pass (usedOnly := true) below, and get nicer induction principles that
-          -- do do not mention odd unused parameters.
+          -- do not mention odd unused parameters.
           -- But the downside is that automatic instantiation of the principle (e.g. in a tactic
           -- that derives them from an function application in the goal) is harder, as
           -- one would have to infer or keep track of which parameters to pass.
diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean
index a2d75aad4f..eb1ad47419 100644
--- a/src/Lean/Meta/Tactic/Intro.lean
+++ b/src/Lean/Meta/Tactic/Intro.lean
@@ -140,7 +140,7 @@ abbrev _root_.Lean.MVarId.introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVa
   introNCore mvarId n [] (useNamesForExplicitOnly := false) (preserveBinderNames := true)
 
 /--
-Introduce one binder using `name` as the the new hypothesis name.
+Introduce one binder using `name` as the new hypothesis name.
 -/
 def _root_.Lean.MVarId.intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do
   let (fvarIds, mvarId) ← mvarId.introN 1 [name]
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
index eb4e3c4d20..a0ae2d71fb 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
@@ -139,7 +139,7 @@ builtin_dsimproc [simp, seval] reduceSub ((_ - _ : BitVec _)) := reduceBin ``HSu
 builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : BitVec _)) := reduceBin ``HDiv.hDiv 6 (· / ·)
 /-- Simplification procedure for the modulo operation on `BitVec`s. -/
 builtin_dsimproc [simp, seval] reduceMod ((_ % _ : BitVec _)) := reduceBin ``HMod.hMod 6 (· % ·)
-/-- Simplification procedure for for the unsigned modulo operation on `BitVec`s. -/
+/-- Simplification procedure for the unsigned modulo operation on `BitVec`s. -/
 builtin_dsimproc [simp, seval] reduceUMod ((umod _ _ : BitVec _)) := reduceBin ``umod 3 umod
 /-- Simplification procedure for unsigned division of `BitVec`s. -/
 builtin_dsimproc [simp, seval] reduceUDiv ((udiv _ _ : BitVec _)) := reduceBin ``udiv 3 udiv
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 400da0ef8a..d5093b18ed 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -308,7 +308,7 @@ with `?m` a fresh metavariable.
 Instance-implicit binder, like `[C]` or `[inst : C]`.
 In regular applications without `@` explicit mode, it is automatically inserted
 and solved for by typeclass inference for the specified class `C`.
-In `@` explicit mode, if `_` is used for an an instance-implicit parameter, then it is still solved for by typeclass inference;
+In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
 use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
 -/
 @[builtin_doc] def instBinder := leading_parser ppGroup <|
@@ -610,7 +610,7 @@ termination_by b c => a - b
 
 By default, a `termination_by` clause will cause the function to be constructed using well-founded
 recursion. The syntax `termination_by structural a` (or `termination_by structural _ c => c`)
-indicates the the function is expected to be structural recursive on the argument. In this case
+indicates the function is expected to be structural recursive on the argument. In this case
 the body of the `termination_by` clause must be one of the function's parameters.
 
 If omitted, a termination argument will be inferred. If written as `termination_by?`,
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index fc5d67b437..3010e46596 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -626,7 +626,7 @@ section MessageHandling
       ctx.chanOut.send <| .responseError id .internalError (toString e) none
       return
 
-    -- we assume that any other request requires at least the the search path
+    -- we assume that any other request requires at least the search path
     -- TODO: move into language-specific request handling
     let t ← IO.bindTask st.srcSearchPathTask fun srcSearchPath => do
       let rc : RequestContext :=
diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean
index 356ecd86da..cc6a1294eb 100644
--- a/src/lake/Lake/CLI/Help.lean
+++ b/src/lake/Lake/CLI/Help.lean
@@ -367,7 +367,7 @@ def helpLean :=
 USAGE:
   lake lean <file> [-- <args>...]
 
-Build the imports of the the given file and then runs `lean` on it using
+Build the imports of the given file and then runs `lean` on it using
 the workspace's root package's additional Lean arguments and the given args
 (in that order). The `lean` process is executed in Lake's environment like
 `lake env lean` (see `lake help env` for how the environment is set up)."
diff --git a/src/lake/Lake/Config/LeanExe.lean b/src/lake/Lake/Config/LeanExe.lean
index 6aff7078dd..dc880b08e5 100644
--- a/src/lake/Lake/Config/LeanExe.lean
+++ b/src/lake/Lake/Config/LeanExe.lean
@@ -53,7 +53,7 @@ namespace LeanExe
   name := self.config.root
   keyName := self.pkg.name ++ self.config.root
 
-/-- Return the the root module if the name matches, otherwise return none. -/
+/-- Return the root module if the name matches, otherwise return none. -/
 def isRoot? (name : Name) (self : LeanExe) : Option Module :=
   if name == self.config.root then some self.root else none
 
diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean
index e07d82f331..7a6af946ec 100644
--- a/src/lake/Lake/Config/LeanLib.lean
+++ b/src/lake/Lake/Config/LeanLib.lean
@@ -101,7 +101,7 @@ Otherwise, falls back to the package's.
 
 /--
 The arguments to pass to `lean --server` when running the Lean language server.
-`serverOptions` is the the accumulation of:
+`serverOptions` is the accumulation of:
 - the package's `leanOptions`
 - the package's `moreServerOptions`
 - the library's `leanOptions`
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index 54e6f6f6fb..30cd46b94b 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -31,7 +31,7 @@ Matches a string that satisfies an arbitrary predicate
 (optionally identified by a `Name`).
 -/
 | satisfies (f : String → Bool) (name := Name.anonymous)
-/-- Matches a string that is a member of the the array -/
+/-- Matches a string that is a member of the array -/
 | mem (xs : Array String)
 /-- Matches a string that starts with this prefix. -/
 | startsWith (pre : String)
diff --git a/src/lake/Lake/Config/Script.lean b/src/lake/Lake/Config/Script.lean
index 79b2fb9080..b80f37a669 100644
--- a/src/lake/Lake/Config/Script.lean
+++ b/src/lake/Lake/Config/Script.lean
@@ -23,7 +23,7 @@ abbrev ScriptFn := (args : List String) → ScriptM ExitCode
 
 /--
 A package `Script` is a `ScriptFn` definition that is
-indexed by a `String` key and can be be run by `lake run <key> [-- <args>]`.
+indexed by a `String` key and can be run by `lake run <key> [-- <args>]`.
 -/
 structure Script where
   /-- The full name of the `Script` (e.g., `pkg/script`). -/
diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean
index e691312104..603ade7e61 100644
--- a/src/lake/Lake/Config/Workspace.lean
+++ b/src/lake/Lake/Config/Workspace.lean
@@ -50,7 +50,7 @@ namespace Workspace
 @[inline] def relLakeDir (self : Workspace) : FilePath :=
   self.root.relLakeDir
 
-/-- The the full path to the workspace's Lake directory (e.g., `.lake`). -/
+/-- The full path to the workspace's Lake directory (e.g., `.lake`). -/
 @[inline] def lakeDir (self : Workspace) : FilePath :=
   self.root.lakeDir
 
diff --git a/src/lake/Lake/Toml/Decode.lean b/src/lake/Lake/Toml/Decode.lean
index 5c2b355944..309db6f697 100644
--- a/src/lake/Lake/Toml/Decode.lean
+++ b/src/lake/Lake/Toml/Decode.lean
@@ -56,7 +56,7 @@ If it fails, add the errors to the state and return `Inhabited.default`.
 /--
 If the value is not `none`, run the decode action.
 If it fails, add the errors to the state and return `none`.
-Otherwise, return the the result in `some`.
+Otherwise, return the result in `some`.
 -/
 @[inline] def optDecode? (a? : Option α)  (f : α → Except (Array ε) β) : StateM (Array ε) (Option β) :=
   optDecodeD none a? fun a  => some <$> f a
diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp
index 3a15b38bfe..35bb6c3754 100644
--- a/src/library/compiler/csimp.cpp
+++ b/src/library/compiler/csimp.cpp
@@ -374,7 +374,7 @@ class csimp_fn {
     }
 
     /* The `float_cases_on` transformation may produce code duplication.
-       The term `e` is "copied" in each branch of the the `cases_on` expression `c`.
+       The term `e` is "copied" in each branch of the `cases_on` expression `c`.
        This method creates one (or more) join-point(s) for `e` (if needed).
        Return `none` if the code size increase is above the threshold.
        Remark: it may produce type incorrect terms. */
@@ -1376,7 +1376,7 @@ class csimp_fn {
     }
 
     /*
-      Given `let x := f as in ... x.i`, where where `f` is defined as
+      Given `let x := f as in ... x.i`, where `f` is defined as
       ```
       def f (xs) :=
       ...
diff --git a/tests/lean/new-compiler/CompilerElimDeadBranches.lean b/tests/lean/new-compiler/CompilerElimDeadBranches.lean
index 12e190918d..047d1ca4e9 100644
--- a/tests/lean/new-compiler/CompilerElimDeadBranches.lean
+++ b/tests/lean/new-compiler/CompilerElimDeadBranches.lean
@@ -22,7 +22,7 @@ This demonstrates that the optimization does do good things to monadic
 code. In this snippet Lean would usually perform a cases on the result
 of `throwMyError` in order to figure out whether it has to:
 - raise an error and exit right now
-- jump to the the `return x + y` continuation
+- jump to the `return x + y` continuation
 Since the abstract interpreter knows that `throwMyError` always returns
 an `Except.error` it will drop the branch where we jump to the continuation.
 This will in turn allow the simplifier to drop the join point that represents
diff --git a/tests/lean/run/rflApplyFoApprox.lean b/tests/lean/run/rflApplyFoApprox.lean
index 9a807cfa7e..974449da50 100644
--- a/tests/lean/run/rflApplyFoApprox.lean
+++ b/tests/lean/run/rflApplyFoApprox.lean
@@ -9,7 +9,7 @@ opaque foo (g : Nat → Nat) (x : Nat) : P x f ↔ Q (g x) := sorry
 example : P x f ↔ Q (x + 10) := by
   rewrite [foo]
   -- we have an mvar now
-  with_reducible rfl -- should should instantiate it with the lambda on the RHS and close the goal
+  with_reducible rfl -- should instantiate it with the lambda on the RHS and close the goal
   -- same as
   -- with_reducible (apply (Iff.refl _))
   -- NB: apply, not exact! Different defEq flags.