style: fix spelling errors in Lean/ docstrings

This PR fixes spelling errors in Lean compiler documentation:
- "occuring" → "occurring" in LibrarySuggestions/Basic.lean (2 occurrences)
- "the the" → "the" in Meta/Match/Match.lean
- "interatively" → "iteratively" in Meta/Match/Match.lean
- "with with" → "with" in DefEqAttrib.lean
- "We we" → "We" in Meta/WHNF.lean
- "of of" → "of" in Shell.lean
- "have have" → "have" in Compiler/LCNF/Specialize.lean

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

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Author: alok

src/Lean/Compiler/LCNF/Specialize.lean

@@ -226,7 +226,7 @@ def shouldSpecialize (specEntry : SpecEntry) (args : Array Arg) : SpecializeM Bo
         If we have `f p` where `p` is a param it makes no sense to specialize as we will just
         close over `p` again and will have made no progress.
 
-        The reason for doing this only for declarations which have have already been specialised
+        The reason for doing this only for declarations which have already been specialised
         themselves is, that we *must* always specialize declarations that are marked with
         `@[specialize]`. This is because the specializer will not specialize their bodies because it
         waits for the bodies to be specialized at the call site. This is for example important in

src/Lean/DefEqAttrib.lean

@@ -56,7 +56,7 @@ Marks the theorem as a definitional equality.
 The theorem must be an equality that holds by `rfl`. This allows `dsimp` to use this theorem
 when rewriting.
 
-A theorem with with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`.
+A theorem with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`.
 To avoid this behavior, write `:= (rfl)` instead.
 
 The attribute should be given before a `@[simp]` attribute to have effect.

src/Lean/Elab/PreDefinition/FixedParams.lean

@@ -462,7 +462,7 @@ def FixedParamPerms.erase  (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
       assert! paramIdx < mapping.size
       if let some fixedParamIdx := mapping[paramIdx]! then
         mask := mask.set! fixedParamIdx true
-  -- Take the transitive closure under under `fixedParamPerms.revDeps`.
+  -- Take the transitive closure under `fixedParamPerms.revDeps`.
   let mut changed := true
   while changed do
     changed := false

src/Lean/LibrarySuggestions/Basic.lean

@@ -92,10 +92,10 @@ end FoldRelevantConstantsImpl
 @[implemented_by FoldRelevantConstantsImpl.foldUnsafe]
 public opaque foldRelevantConstants {α : Type} (e : Expr) (init : α) (f : Name → α → MetaM α) : MetaM α := pure init
 
-/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstants (e : Expr) : MetaM (Array Name) := foldRelevantConstants e #[] (fun n ns => return ns.push n)
 
-/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstantsAsSet (e : Expr) : MetaM NameSet := foldRelevantConstants e ∅ (fun n ns => return ns.insert n)
 
 end Lean.Expr

src/Lean/Meta/Match/Match.lean

@@ -22,9 +22,9 @@ import Lean.Meta.Match.NamedPatterns
 
 /-!
 This module implements the backend of match compilation. The elaborator has already elaborated
-the patterns and the the expected type of the matcher is known.
+the patterns and the expected type of the matcher is known.
 
-The match compilation task is represented as a `Problem`, which is then processed interatively by
+The match compilation task is represented as a `Problem`, which is then processed iteratively by
 the `process` function. It has various “moves” which it tries in a particular order, to make progress
 on the problem, possibly splitting it.
 

src/Lean/Meta/WHNF.lean

@@ -210,7 +210,7 @@ private def isWFRec (declName : Name) : Bool :=
 /--
 Helper method for `reduceRec`.
 We use it to ensure we don't expose `Nat.add` when reducing `Nat.rec`.
-We we use the following trick, if `e` can be expressed as an offset `(a, k)` with `k > 0`,
+We use the following trick: if `e` can be expressed as an offset `(a, k)` with `k > 0`,
 we create a new expression `Nat.succ e'` where `e'` is `a` for `k = 1`, or `a + (k-1)` for `k > 1`.
 See issue #3022
 -/

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -33,7 +33,7 @@ def findCompletionCmdDataAtPos
     : ServerTask (Option (Syntax × Elab.InfoTree)) :=
   -- `findCmdDataAtPos` may produce an incorrect snapshot when `pos` is in whitespace.
   -- However, most completions don't need trailing whitespace at the term level;
-  -- synthetic completions are the only notions of completion that care care about whitespace.
+  -- synthetic completions are the only notions of completion that care about whitespace.
   -- Synthetic tactic completion only needs the `ContextInfo` of the command, so any snapshot
   -- will do.
   -- Synthetic field completion in `{ }` doesn't care about whitespace;

src/Lean/Shell.lean

@@ -108,7 +108,7 @@ opaque Internal.enableDebug (tag : @& String) : BaseIO Unit
 /--
 Lean's short version string (i.e., what is printed by `lean --short-version`).
 
-This is the Lean equivalent of of the C++ `LEAN_VERSION_STRING` / `g_short_version_string`.
+This is the Lean equivalent of the C++ `LEAN_VERSION_STRING` / `g_short_version_string`.
 -/
 def shortVersionString : String :=
   if version.specialDesc ≠ "" then