chore: minor String improvements (#10891)

This PR renames the cast functions on `String.ValidPos` for `set` and
`modify` to adhere to the established naming convention.

It also fixes two typos and very slighly tweaks the import graph,
shortening the critical path by a negligible amount.

src/Init/Data/String/Basic.lean

@@ -1674,7 +1674,7 @@ def Slice.Pos.ofSlice {s : String} (pos : s.toSlice.Pos) : s.ValidPos where
   isValid := pos.isValidForSlice.ofSlice
 
 @[simp]
-theorem Slice.Pos.ofset_ofSlice {s : String} {pos : s.toSlice.Pos} : pos.ofSlice.offset = pos.offset := (rfl)
+theorem Slice.Pos.offset_ofSlice {s : String} {pos : s.toSlice.Pos} : pos.ofSlice.offset = pos.offset := (rfl)
 
 @[simp]
 theorem rawEndPos_toSlice {s : String} : s.toSlice.rawEndPos = s.rawEndPos := by
@@ -2538,14 +2538,14 @@ theorem Pos.Raw.IsValid.set_of_le {s : String} {p : s.ValidPos} {c : Char} {hp :
 /-- Given a valid position in a string, obtain the corresponding position after setting a character on
 that string, provided that the position was before the changed position. -/
 @[inline]
-def ValidPos.setOfLE {s : String} (q p : s.ValidPos) (c : Char) (hp : p ≠ s.endValidPos)
+def ValidPos.toSetOfLE {s : String} (q p : s.ValidPos) (c : Char) (hp : p ≠ s.endValidPos)
     (hpq : q ≤ p) : (p.set c hp).ValidPos where
   offset := q.offset
   isValid := q.isValid.set_of_le hpq
 
 @[simp]
-theorem ValidPos.offset_setOfLE {s : String} {q p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos}
-    {hpq : q ≤ p} : (q.setOfLE p c hp hpq).offset = q.offset := (rfl)
+theorem ValidPos.offset_toSetOfLE {s : String} {q p : s.ValidPos} {c : Char} {hp : p ≠ s.endValidPos}
+    {hpq : q ≤ p} : (q.toSetOfLE p c hp hpq).offset = q.offset := (rfl)
 
 /--
 Replaces the character at position `p` in the string `s` with the result of applying `f` to that
@@ -2568,14 +2568,14 @@ theorem Pos.Raw.IsValid.modify_of_le {s : String} {p : s.ValidPos} {f : Char →
 
 /-- Given a valid position in a string, obtain the corresponding position after modifying a character
 in that string, provided that the position was before the changed position. -/
-def ValidPos.modifyOfLE {s : String} (q p : s.ValidPos) (f : Char → Char)
+def ValidPos.toModifyOfLE {s : String} (q p : s.ValidPos) (f : Char → Char)
     (hp : p ≠ s.endValidPos) (hpq : q ≤ p) : (p.modify f hp).ValidPos where
   offset := q.offset
   isValid := q.isValid.modify_of_le hpq
 
 @[simp]
-theorem ValidPos.offset_modifyOfLE {s : String} {q p : s.ValidPos} {f : Char → Char}
-    {hp : p ≠ s.endValidPos} {hpq : q ≤ p} : (q.modifyOfLE p f hp hpq).offset = q.offset := (rfl)
+theorem ValidPos.offset_toModifyOfLE {s : String} {q p : s.ValidPos} {f : Char → Char}
+    {hp : p ≠ s.endValidPos} {hpq : q ≤ p} : (q.toModifyOfLE p f hp hpq).offset = q.offset := (rfl)
 
 /--
 Replaces the character at a specified position in a string with a new character. If the position is

src/Init/Data/ToString/Name.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura and Sebastian Ullrich
 module
 
 prelude
-public import Init.Data.String.Extra
+public import Init.Data.String.Basic
 
 /-!
 Here we give the. implementation of `Name.toString`. There is also a private implementation in

src/Init/System/IO.lean

@@ -9,7 +9,6 @@ prelude
 public import Init.System.IOError
 public import Init.System.FilePath
 public import Init.Data.Ord.UInt
-public import Init.Data.String.Extra
 
 public section
 

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -26,7 +26,7 @@ This module finds lexicographic termination measures for well-founded recursion.
 
 Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), and complex measures
 (e.g. `e₂ - e₁` if `e₁ < e₂` is found in the context of a recursive call) it tries all combinations
-until it finds one where all proof obligations go through with the given tactic (`decerasing_by`),
+until it finds one where all proof obligations go through with the given tactic (`decreasing_by`),
 if given, or the default `decreasing_tactic`.
 
 For mutual recursion, a single measure is not just one parameter, but one from each recursive