s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ i.byteIdx <
    (ite (s.startPos + i = s.stopPos) i
        { byteIdx := (String.next s.str (s.startPos + i)).byteIdx - s.startPos.byteIdx }).byteIdx
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ i.byteIdx < (next s i).byteIdx
simp [next]
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ i.byteIdx < { byteIdx := (String.next s.str (s.startPos + i)).byteIdx - s.startPos.byteIdx }.byteIdx

case a
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ ¬s.startPos + i = s.stopPos
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ i.byteIdx <
    (ite (s.startPos + i = s.stopPos) i
        { byteIdx := (String.next s.str (s.startPos + i)).byteIdx - s.startPos.byteIdx }).byteIdx
rw [if_neg ?a]
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ i.byteIdx < { byteIdx := (String.next s.str (s.startPos + i)).byteIdx - s.startPos.byteIdx }.byteIdx
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ i.byteIdx < { byteIdx := (String.next s.str (s.startPos + i)).byteIdx - s.startPos.byteIdx }.byteIdx

case a
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ ¬s.startPos + i = s.stopPos
case a =>
  refine mt (congrArg String.Pos.byteIdx) (Nat.ne_of_lt ?_)
  exact (Nat.add_comm .. ▸ Nat.add_lt_of_lt_sub h :)
case h
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ i.byteIdx + s.startPos.byteIdx < (String.next s.str (s.startPos + i)).byteIdx
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ i.byteIdx < { byteIdx := (String.next s.str (s.startPos + i)).byteIdx - s.startPos.byteIdx }.byteIdx
apply Nat.lt_sub_of_add_lt
case h
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ s.startPos.byteIdx + i.byteIdx < (String.next s.str (s.startPos + i)).byteIdx
case h
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ i.byteIdx + s.startPos.byteIdx < (String.next s.str (s.startPos + i)).byteIdx
rw [Nat.add_comm]
no goals
case h
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ s.startPos.byteIdx + i.byteIdx < (String.next s.str (s.startPos + i)).byteIdx
apply String.lt_next
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ (s.startPos + i).byteIdx < s.stopPos.byteIdx
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ ¬s.startPos + i = s.stopPos
refine mt (congrArg String.Pos.byteIdx) (Nat.ne_of_lt ?_)
no goals
s : Substring
i : String.Pos
h : i.byteIdx < bsize s
⊢ (s.startPos + i).byteIdx < s.stopPos.byteIdx
exact (Nat.add_comm .. ▸ Nat.add_lt_of_lt_sub h :)