no goals
s : String
p : Pos
h : Pos.Valid s p
h₂ : p < endPos s
⊢ Pos.Valid s (next s p)
match s, p, h with
| ⟨_⟩, ⟨_⟩, ⟨cs, [], rfl, rfl⟩ => simp at h₂
| ⟨_⟩, ⟨_⟩, ⟨cs, c::cs', rfl, rfl⟩ =>
  rw [utf8ByteSize.go_eq, next_of_valid]
  simpa using Pos.Valid.mk (cs ++ [c]) cs'
no goals
s : String
p : Pos
h : Pos.Valid s p
cs : List Char
h₂ : { byteIdx := utf8ByteSize.go cs } < endPos { data := cs ++ [] }
⊢ Pos.Valid { data := cs ++ [] } (next { data := cs ++ [] } { byteIdx := utf8ByteSize.go cs })
simp at h₂
s : String
p : Pos
h : Pos.Valid s p
cs : List Char
c : Char
cs' : List Char
h₂ : { byteIdx := utf8ByteSize.go cs } < endPos { data := cs ++ c :: cs' }
⊢ Pos.Valid { data := cs ++ c :: cs' } { byteIdx := utf8Len cs + csize c }
s : String
p : Pos
h : Pos.Valid s p
cs : List Char
c : Char
cs' : List Char
h₂ : { byteIdx := utf8ByteSize.go cs } < endPos { data := cs ++ c :: cs' }
⊢ Pos.Valid { data := cs ++ c :: cs' } (next { data := cs ++ c :: cs' } { byteIdx := utf8ByteSize.go cs })
rw [utf8ByteSize.go_eq, next_of_valid]
no goals
s : String
p : Pos
h : Pos.Valid s p
cs : List Char
c : Char
cs' : List Char
h₂ : { byteIdx := utf8ByteSize.go cs } < endPos { data := cs ++ c :: cs' }
⊢ Pos.Valid { data := cs ++ c :: cs' } { byteIdx := utf8Len cs + csize c }
simpa using Pos.Valid.mk (cs ++ [c]) cs'