x✝ : Iterator
h✝ : Valid x✝
hn : hasNext x✝ = true
l r : List Char
h : ValidFor l r x✝
⊢ Valid (Iterator.next x✝)
x✝ : Iterator
h : Valid x✝
hn : hasNext x✝ = true
⊢ Valid (Iterator.next x✝)
let ⟨l, r, h⟩ := h.validFor
case intro.intro
x✝ : Iterator
h✝ : Valid x✝
hn : hasNext x✝ = true
l : List Char
c : Char
r : List Char
h : ValidFor l (c :: r) x✝
⊢ Valid (Iterator.next x✝)
x✝ : Iterator
h✝ : Valid x✝
hn : hasNext x✝ = true
l r : List Char
h : ValidFor l r x✝
⊢ Valid (Iterator.next x✝)
obtain ⟨c, r, rfl⟩ := List.exists_cons_of_ne_nil (h.hasNext.1 hn)
no goals
case intro.intro
x✝ : Iterator
h✝ : Valid x✝
hn : hasNext x✝ = true
l : List Char
c : Char
r : List Char
h : ValidFor l (c :: r) x✝
⊢ Valid (Iterator.next x✝)
exact h.next.valid