diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index ed27c3d05e..588646208a 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -243,6 +243,9 @@ def next : Iterator → Iterator
 def prev : Iterator → Iterator
   | ⟨s, i⟩ => ⟨s, s.prev i⟩
 
+def atEnd : Iterator → Bool
+  | ⟨s, i⟩ => i.byteIdx ≥ s.endPos.byteIdx
+
 def hasNext : Iterator → Bool
   | ⟨s, i⟩ => i.byteIdx < s.endPos.byteIdx
 
diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean
index a1e3ef8b91..707337ed2d 100644
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@@ -48,7 +48,7 @@ theorem eq_empty_of_bsize_eq_zero (h : s.endPos = {}) : s = "" := by
 theorem lt_next (s : String) (i : String.Pos) : i.1 < (s.next i).1 := by
   simp_arith [next]; apply one_le_csize
 
-theorem Iterator.sizeOf_next_lt (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i := by
+theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i := by
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
   have := String.lt_next s pos
   apply Nat.sub.elim (motive := fun k => k < _) (utf8ByteSize s) (String.next s pos).1
@@ -58,6 +58,12 @@ theorem Iterator.sizeOf_next_lt (i : String.Iterator) (h : i.hasNext) : sizeOf i
     simp_all_arith
   . intro; apply Nat.zero_lt_sub_of_lt h
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt; assumption)
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
+
+theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
+  have h : i.hasNext = true := by simp_arith [atEnd] at h; simp_arith [hasNext, h]
+  sizeOf_next_lt_of_hasNext i h
+
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
 
 end String
diff --git a/tests/lean/run/lex.lean b/tests/lean/run/lex.lean
index f82cbb87f0..0bb01d7df3 100644
--- a/tests/lean/run/lex.lean
+++ b/tests/lean/run/lex.lean
@@ -28,7 +28,9 @@ def Char.digit? (char : Char) : Option Nat :=
 
 mutual
   def lex [Monad m] [MonadExceptOf LexErr m] (it : String.Iterator) : m (List Token) := do
-    if it.hasNext then
+    if it.atEnd then
+      return []
+    else
       match it.curr with
       | '(' => return { text := "(", tok := Tok.lpar } :: (← lex it.next)
       | ')' => return { text := ")", tok := Tok.rpar } :: (← lex it.next)
@@ -37,17 +39,15 @@ mutual
         match other.digit? with
         | none   => throw <| LexErr.unexpected other
         | some d => lexnumber d [other] it.next
-    else
-      return []
 
   def lexnumber [Monad m] [MonadExceptOf LexErr m] (soFar : Nat) (text : List Char) (it : String.Iterator) : m (List Token) :=
-    if it.hasNext then
+    if it.atEnd then
+      return [{ text := text.reverse.asString, tok := Tok.num soFar }]
+    else
       let c := it.curr
       match c.digit? with
       | none   => return { text := text.reverse.asString, tok := Tok.num soFar } :: (← lex it)
       | some d => lexnumber (soFar * 10 + d) (c :: text) it.next
-    else
-      return [{ text := text.reverse.asString, tok := Tok.num soFar }]
 end
 
 #eval lex (m := Except LexErr) "".iter
@@ -64,7 +64,9 @@ namespace NonMutual
 def lex [Monad m] [MonadExceptOf LexErr m] (current? : Option (List Char × Nat)) (it : String.Iterator) : m (List Token) := do
   let currTok := fun
     | (cs, n) => { text := {data := cs.reverse}, tok := Tok.num n }
-  if it.hasNext then
+  if it.atEnd then
+    return current?.toList.map currTok
+  else
     let emit (tok : Token) (xs : List Token) : List Token :=
       match current? with
       | none => tok :: xs
@@ -79,8 +81,6 @@ def lex [Monad m] [MonadExceptOf LexErr m] (current? : Option (List Char × Nat)
           | some d => match current? with
             | none => lex (some ([other], d)) it.next
             | some (tokTxt, soFar) => lex (other :: tokTxt, soFar * 10 + d) it.next
-  else
-    return current?.toList.map currTok
 
 #eval lex (m := Except LexErr) none "".iter
 #eval lex (m := Except LexErr) none "123".iter