chore: fix spelling (#11531)

Hi, these are just some spelling corrections.

There is one I wasn't completely sure about in
src/Init/Data/List/Lemmas.lean:

> See also
> ...
> Also
> \* \`Init.Data.List.Monadic\` for **addiation** _(additional?)_ lemmas
about \`List.mapM\` and \`List.forM\`

Author: tom93

src/Init/Data/BitVec/Bitblast.lean

@@ -835,7 +835,7 @@ execution. -/
 structure DivModArgs (w : Nat) where
   /-- the numerator (aka, dividend) -/
   n : BitVec w
-  /-- the denumerator (aka, divisor)-/
+  /-- the denominator (aka, divisor)-/
   d : BitVec w
 
 /-- A `DivModState` is lawful if the remainder width `wr` plus the numerator width `wn` equals `w`,

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/Bool.lean

@@ -260,7 +260,7 @@ instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
 
 theorem eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y := by decide
 
-/-! ### coercision related normal forms -/
+/-! ### coercion related normal forms -/
 
 theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
     (a == b) = decide (a = b) := 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/Data/List/Lemmas.lean

@@ -77,7 +77,7 @@ Further results, which first require developing further automation around `Nat`,
 * `Init.Data.List.Nat.TakeDrop`: `List.take` and `List.drop`
 
 Also
-* `Init.Data.List.Monadic` for addiation lemmas about `List.mapM` and `List.forM`.
+* `Init.Data.List.Monadic` for additional lemmas about `List.mapM` and `List.forM`.
 
 -/
 

src/Init/Data/List/Sublist.lean

@@ -249,7 +249,7 @@ theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l
   | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _)
   | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)]
 
--- Only activative `eq_of_length` if we're already thinking about lengths.
+-- Only activate `eq_of_length` if we're already thinking about lengths.
 grind_pattern Sublist.eq_of_length => l₁ <+ l₂, length l₁, length l₂
 
 theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l₁) : l₁ = l₂ :=

src/Init/Data/String/Basic.lean

@@ -1177,7 +1177,7 @@ position. -/
 def Slice.Pos.get? {s : Slice} (pos : s.Pos) : Option Char :=
   if h : pos = s.endPos then none else some (pos.get h)
 
-/-- Returns the byte at the given position in the string, or panicks if the position is the end
+/-- Returns the byte at the given position in the string, or panics if the position is the end
 position. -/
 @[expose]
 def Slice.Pos.get! {s : Slice} (pos : s.Pos) : Char :=

src/Init/Data/String/Decode.lean

@@ -529,7 +529,7 @@ public def assemble₂ (w x : UInt8) : Option Char :=
   else
     let r := assemble₂Unchecked w x
     if r < 0x80 then
-      none -- overlong encodinlg
+      none -- overlong encoding
     else
       some ⟨r, ?onemore⟩
 where finally

src/Init/Data/UInt/Basic.lean

@@ -517,7 +517,7 @@ protected def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (UI
 Strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
 natural numbers. Usually accessed via the `<` operator.
 -/
--- These need to be exposed as `Init.Prelude` already has an instance for bootstrapping puproses and
+-- These need to be exposed as `Init.Prelude` already has an instance for bootstrapping purposes and
 -- they should be defeq
 @[expose] protected def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
 /--

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.