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

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

Co-Authored-By: Claude Opus 4.5 <[email protected]>

Author: alok

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/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/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