it : Iterator
⊢ ValidFor (List.reverse it.s.data) [] { s := it.s, i := endPos it.s }
it : Iterator
⊢ ValidFor (List.reverse it.s.data) [] (Iterator.toEnd it)
simp [Iterator.toEnd]
no goals
it : Iterator
⊢ ValidFor (List.reverse it.s.data) [] { s := it.s, i := endPos it.s }
exact .of_eq _ (by simp [List.reverseAux_eq]) (by simp [endPos, utf8ByteSize])
no goals
it : Iterator
⊢ { s := it.s, i := endPos it.s }.s.data = List.reverseAux (List.reverse it.s.data) []
simp [List.reverseAux_eq]
no goals
it : Iterator
⊢ { s := it.s, i := endPos it.s }.i.byteIdx = utf8Len (List.reverse it.s.data)
simp [endPos, utf8ByteSize]