doc: correct typos in documentation and comments (#11465)

This PR fixes various typos across the codebase in documentation and
comments.

- `infered` → `inferred` (ParserCompiler.lean)
- `declartation` → `declaration` (Cleanup.lean)
- `certian` → `certain` (CasesInfo.lean)
- `wil` → `will` (Cache.lean)
- `the the` → `the` (multiple files - PrefixTree.lean, Sum/Basic.lean,
List/Nat/Perm.lean, Time.lean, Bounded.lean, Lake files)
- `to to` → `to` (MutualInductive.lean, simp_bubblesort_256.lean)
- Grammar improvements in Bounded.lean and Time.lean

All changes are to comments and documentation only - no functional
changes.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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

Author: alok

src/Init/Data/List/Nat/Perm.lean

@@ -60,14 +60,14 @@ theorem set_set_perm {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : j
 
 namespace Perm
 
-/-- Variant of `List.Perm.take` specifying the the permutation is constant after `i` elementwise. -/
+/-- Variant of `List.Perm.take` specifying that the permutation is constant after `i` elementwise. -/
 theorem take_of_getElem? {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, i ≤ j → l₁[j]? = l₂[j]?) :
     l₁.take i ~ l₂.take i := by
   refine h.take (Perm.of_eq ?_)
   ext1 j
   simpa using w (i + j) (by omega)
 
-/-- Variant of `List.Perm.drop` specifying the the permutation is constant before `i` elementwise. -/
+/-- Variant of `List.Perm.drop` specifying that the permutation is constant before `i` elementwise. -/
 theorem drop_of_getElem? {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, j < i → l₁[j]? = l₂[j]?) :
     l₁.drop i ~ l₂.drop i := by
   refine h.drop (Perm.of_eq ?_)

src/Init/Data/Sum/Basic.lean

@@ -13,7 +13,7 @@ public section
 /-!
 # Disjoint union of types
 
-This file defines basic operations on the the sum type `α ⊕ β`.
+This file defines basic operations on the sum type `α ⊕ β`.
 
 `α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.
 

src/Lean/Data/PrefixTree.lean

@@ -52,7 +52,7 @@ partial def find? (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp)
       | some t => loop t ks
   loop t k
 
-/-- Returns the the value of the longest key in `t` that is a prefix of `k`, if any. -/
+/-- Returns the value of the longest key in `t` that is a prefix of `k`, if any. -/
 @[inline]
 partial def findLongestPrefix? (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) (k : List α) : Option β :=
   let rec @[specialize] loop acc?

src/Lean/Elab/MutualInductive.lean

@@ -1173,7 +1173,7 @@ private def checkNoInductiveNameConflicts (elabs : Array InductiveElabStep1) (is
   let throwErrorsAt (init cur : Syntax) (msg : MessageData) : TermElabM Unit := do
     logErrorAt init msg
     throwErrorAt cur msg
-  -- Maps names of inductive types to to `true` and those of constructors to `false`, along with syntax refs
+  -- Maps names of inductive types to `true` and those of constructors to `false`, along with syntax refs
   let mut uniqueNames : Std.HashMap Name (Bool × Syntax) := {}
   let declString := if isCoinductive then "coinductive predicate" else "inductive type"
   trace[Elab.inductive] "deckString: {declString}"

src/Lean/Meta/CasesInfo.lean

@@ -26,7 +26,7 @@ It is used in particular by the code generator to replace calls to such function
 `cases` construct.
 
 The `getSparseCasesInfo?` function calculates the `CasesInfo` from the type of the declaration, and
-makes certian assumptions about their shapes. If this is too fragile, the `sparseCasesOn` env
+makes certain assumptions about their shapes. If this is too fragile, the `sparseCasesOn` env
 extension could carry more information from which the shape can be calculated..
 -/
 

src/Lean/Meta/Tactic/Cleanup.lean

@@ -72,7 +72,7 @@ where
   - It occurs in the target type, or
   - There is a relevant variable `y` that depends on `x`, or
   - If `indirectProps` is true, the type of `x` is a proposition and it depends on a relevant variable `y`.
-  - If `indirectProps` is true, `x` is a local declartation and its value mentions a relevant variable `y`.
+  - If `indirectProps` is true, `x` is a local declaration and its value mentions a relevant variable `y`.
 
   By default, `toPreserve := #[]` and `indirectProps := true`. These settings are used in the mathlib tactic `extract_goal`
   to give the user more control over which variables to include.

src/Lean/ParserCompiler.lean

@@ -107,7 +107,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
           name := c', levelParams := []
           type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe
         }
-        -- usually `meta` is infered during compilation for auxiliary definitions, but as
+        -- usually `meta` is inferred during compilation for auxiliary definitions, but as
         -- `ctx.combinatorAttr` may enforce correct use of the modifier, infer now.
         if isMarkedMeta (← getEnv) c then
           modifyEnv (markMeta · c')

src/Std/Time.lean

@@ -171,7 +171,7 @@ The supported formats include:
   - `EEEE`: Displays the full day name (e.g., "Tuesday").
   - `EEEEE`: Displays the narrow day name (e.g., "T" for Tuesday).
 - `e`: Represents the weekday as number or text.
-  - `e`, `ee`: Displays the the as a number, starting from 1 (Monday) to 7 (Sunday).
+  - `e`, `ee`: Displays the weekday as a number, starting from 1 (Monday) to 7 (Sunday).
   - `eee`, `eeee`, `eeeee`: Displays the weekday as text (same format as `E`).
 - `F`: Represents the week of the month that the first week starts on the first day of the month (e.g., "3").
 - `a`: Represents the AM or PM designation of the day.

src/Std/Time/Internal/Bounded.lean

@@ -61,7 +61,7 @@ instance : LawfulEqOrd (Bounded rel n m) where
 variable {rel a b}
 
 /--
-A `Bounded` integer that the relation used is the the less-equal relation so, it includes all
+A `Bounded` integer where the relation used is the less-equal relation, so it includes all
 integers that `lo ≤ val ≤ hi`.
 -/
 abbrev LE := @Bounded LE.le
@@ -74,7 +74,7 @@ def cast {rel : Int → Int → Prop} {lo₁ lo₂ hi₁ hi₂ : Int} (h₁ : lo
   .mk b.val ⟨h₁ ▸ b.property.1, h₂ ▸ b.property.2⟩
 
 /--
-A `Bounded` integer that the relation used is the the less-than relation so, it includes all
+A `Bounded` integer where the relation used is the less-than relation, so it includes all
 integers that `lo < val < hi`.
 -/
 abbrev LT := @Bounded LT.lt

src/lake/Lake/Build/Common.lean

@@ -499,7 +499,7 @@ public class ResolveOutputs (m : Type v → Type w) (α : Type v) where
 
 open ResolveOutputs in
 /--
-Retrieve artifacts from the Lake cache using the the outputs stored
+Retrieve artifacts from the Lake cache using the outputs stored
 in either the saved trace file or in the cached input-to-content mapping.
 
 **For internal use only.**