fix: remove extra universe parameter fromStd.Iter.intercalateString (#13092)

This PR fixes an issue where `Std.Iter.joinString` had an extra universe
parameter because of an `IteratorLoop` instance which was actually
unnecessary.

src/Init/Data/String/Iter/Intercalate.lean

@@ -17,7 +17,7 @@ namespace Std
 /--
 Appends all the elements in the iterator, in order.
 -/
-public def Iter.joinString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
+public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
     (it : Std.Iter (α := α) β) : String :=
   (it.map toString).fold (init := "") (· ++ ·)
 
@@ -25,7 +25,7 @@ public def Iter.joinString {α β : Type} [Iterator α Id β] [IteratorLoop α I
 Appends the elements of the iterator into a string, placing the separator {name}`s` between them.
 -/
 @[inline]
-public def Iter.intercalateString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
+public def Iter.intercalateString {α β : Type} [Iterator α Id β] [ToString β]
     (s : String.Slice) (it : Std.Iter (α := α) β) : String :=
   it.map toString
     |>.fold (init := none) (fun

src/Init/Data/String/Lemmas/Iter.lean

@@ -18,14 +18,13 @@ namespace Std.Iter
 
 @[simp]
 public theorem joinString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β]
-    {it : Std.Iter (α := α) β} : it.joinString = String.join (it.toList.map toString) := by
+    [ToString β] {it : Std.Iter (α := α) β} :
+    it.joinString = String.join (it.toList.map toString) := by
   rw [joinString, String.join, ← foldl_toList, toList_map]
 
 @[simp]
 public theorem intercalateString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β] {s : String.Slice}
-    {it : Std.Iter (α := α) β} :
+    [ToString β] {s : String.Slice} {it : Std.Iter (α := α) β} :
     it.intercalateString s = s.copy.intercalate (it.toList.map toString) := by
   simp only [intercalateString, String.appendSlice_eq, ← foldl_toList, toList_map]
   generalize s.copy = s