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

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

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

Author: alok

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.