Theorem: String.Iterator.Valid.next' (RegexCorrectness/Data/String.lean)

State before:
it : Iterator
v : it.Valid
h : ¬it.atEnd = true
⊢ it.next.Valid
Tactic:
apply v.next
State after:
it : Iterator
v : it.Valid
h : ¬it.atEnd = true
⊢ it.hasNext = true

State before:
it : Iterator
v : it.Valid
h : ¬it.atEnd = true
⊢ it.hasNext = true
Tactic:
simp [hasNext, atEnd] at *
State after:
it : Iterator
v : it.Valid
h : it.i.byteIdx < it.s.endPos.byteIdx
⊢ it.i.byteIdx < it.s.endPos.byteIdx

State before:
it : Iterator
v : it.Valid
h : it.i.byteIdx < it.s.endPos.byteIdx
⊢ it.i.byteIdx < it.s.endPos.byteIdx
Tactic:
exact h
State after:
no goals