chore: fix spelling ("the the")

Author: tom93

src/Init/Data/BitVec/Lemmas.lean

@@ -5601,7 +5601,7 @@ theorem msb_eq_toNat {x : BitVec w}:
   simp only [msb_eq_decide, ge_iff_le]
 
 /-- Negating a bitvector created from a natural number equals
-creating a bitvector from the the negative of that number.
+creating a bitvector from the negative of that number.
 -/
 theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} :
     - BitVec.ofNat w x = BitVec.ofInt w (- x) := by

src/Init/Data/List/Basic.lean

@@ -2252,7 +2252,7 @@ def eraseReps {α} [BEq α] (as : List α) : List α := eraseRepsBy (· == ·) a
 /-! ### span -/
 
 /--
-Splits a list into the the longest initial segment for which `p` returns `true`, paired with the
+Splits a list into the longest initial segment for which `p` returns `true`, paired with the
 remainder of the list.
 
 `O(|l|)`.

src/Init/System/IO.lean

@@ -837,7 +837,7 @@ Encountering an EOF does not close a handle. Subsequent reads may block and retu
 -/
 @[extern "lean_io_prim_handle_read"] opaque read (h : @& Handle) (bytes : USize) : IO ByteArray
 /--
-Writes the provided bytes to the the handle.
+Writes the provided bytes to the handle.
 
 Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use
 `IO.FS.Handle.flush` to write changes to buffers to the associated device.

src/Init/Tactics.lean

@@ -1004,7 +1004,7 @@ You can use `with` to provide the variables names for each constructor.
 syntax (name := cases) "cases " elimTarget,+ (" using " term)? (inductionAlts)? : tactic
 
 /--
-The `fun_induction` tactic is a convenience wrapper around the `induction` tactic to use the the
+The `fun_induction` tactic is a convenience wrapper around the `induction` tactic to use the
 functional induction principle.
 
 The tactic invocation

src/Lean/Elab/PreDefinition/FixedParams.lean

@@ -307,7 +307,7 @@ def FixedParamPerm.isFixed (perm : FixedParamPerm) (i : Nat) : Bool :=
   perm[i]?.join.isSome
 
 /--
-Brings the fixed parameters from `type`, which should the the type of the `funIdx`'s function, into
+Brings the fixed parameters from `type`, which should be the type of the `funIdx`'s function, into
 scope.
 -/
 private partial def FixedParamPerm.forallTelescopeImpl (perm : FixedParamPerm)

src/Lean/Elab/StructInst.lean

@@ -804,7 +804,7 @@ private def synthOptParamFields : StructInstM Unit := do
           /-
           We must use `checkedAssign` here to ensure we do not create a cyclic
           assignment. See #3150.
-          This can happen when there are holes in the the fields the default value
+          This can happen when there are holes in the fields the default value
           depends on.
           Possible improvement: create a new `_` instead of returning `false` when
           `checkedAssign` fails. Reason: the field will not be needed after the

src/Lean/Elab/Tactic/Induction.lean

@@ -49,7 +49,7 @@ def getAltName? (alt : Syntax) : Option Name :=
   else
     let ident := head[1]
     if ident.isOfKind identKind then some ident.getId.eraseMacroScopes else none
-/-- Returns true if the the alternative is for a wildcard, and that the wildcard is not due to a syntax error. -/
+/-- Returns true if the alternative is for a wildcard, and that the wildcard is not due to a syntax error. -/
 def isAltWildcard (altStx : Syntax) : Bool :=
   getAltName? altStx == some `_
 /-- Returns the `inductionAlt` `ident <|> hole` -/
@@ -233,7 +233,7 @@ public partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag :
 
 /--
 Given a goal `... targets ... |- C[targets, complexArgs]` associated with `mvarId`,
-where `complexArgs` are the the complex (i.e. non-target) arguments to the motive in the conclusion
+where `complexArgs` are the complex (i.e. non-target) arguments to the motive in the conclusion
 of the eliminator, construct `motiveArg := fun targets rs => C[targets, rs]`
 
 This checks if the type of the complex arguments match what's expected by the motive, and

src/Lean/Meta/Basic.lean

@@ -1867,7 +1867,7 @@ def withLetDecl (name : Name) (type : Expr) (val : Expr) (k : Expr → n α) (no
 /--
 Runs `k x` with the local declaration `<name> : <type> := <val>` added to the local context, where `x` is the new free variable.
 Afterwards, the result is wrapped in the given `let`/`have` expression (according to the value of `nondep`).
-- If `usedLetOnly := true` (the default) then the the `let`/`have` is not created if the variable is unused.
+- If `usedLetOnly := true` (the default) then the `let`/`have` is not created if the variable is unused.
 -/
 def mapLetDecl [MonadLiftT MetaM n] (name : Name) (type : Expr) (val : Expr) (k : Expr → n Expr) (nondep : Bool := false) (kind : LocalDeclKind := .default) (usedLetOnly : Bool := true) : n Expr :=
   withLetDecl name type val (nondep := nondep) (kind := kind) fun x => do

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -61,7 +61,7 @@ def addCongrTable (e : Expr) : GoalM Unit := do
       pushEqHEq e e' congrPlaceholderProof
     if (← swapCgrRepr e e') then
       /-
-      Recall that `isDiseq` and `mkDiseqProof?` are implemented using the the congruence table.
+      Recall that `isDiseq` and `mkDiseqProof?` are implemented using the congruence table.
       So, if `e` is an equality `a = b`, and is the equivalence class of `False`, but `e'` is not,
       we **must** make `e` the representative of the congruence class.
       The equivalence classes of `e` and `e'` will be merged eventually since we used `pushEqHEq` above,

tests/lean/grind/experiments/bitvec.lean

@@ -5190,7 +5190,7 @@ theorem msb_eq_toNat {x : BitVec w}:
   simp only [msb_eq_decide, ge_iff_le]
 
 /-- Negating a bitvector created from a natural number equals
-creating a bitvector from the the negative of that number.
+creating a bitvector from the negative of that number.
 -/
 theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} :
     - BitVec.ofNat w x = BitVec.ofInt w (- x) := by