no goals
t : List Char
i : Nat
⊢ go₂ ([] ++ t) { byteIdx := i } { byteIdx := utf8Len [] + i } = []
cases t <;> simp [go₂]
c : Char
cs t : List Char
i : Nat
⊢ go₂ (cs ++ t) { byteIdx := i + csize c } { byteIdx := utf8Len cs + csize c + i } = cs
c : Char
cs t : List Char
i : Nat
⊢ go₂ (c :: cs ++ t) { byteIdx := i } { byteIdx := utf8Len (c :: cs) + i } = c :: cs
simp [go₂, Pos.ext_iff, ne_add_csize_add_self, Pos.addChar_eq]
case a
c : Char
cs t : List Char
i : Nat
⊢ utf8Len cs + csize c + i = utf8Len cs + (i + csize c)
c : Char
cs t : List Char
i : Nat
⊢ go₂ (cs ++ t) { byteIdx := i + csize c } { byteIdx := utf8Len cs + csize c + i } = cs
apply go₂_append_left
no goals
case a
c : Char
cs t : List Char
i : Nat
⊢ utf8Len cs + csize c + i = utf8Len cs + (i + csize c)
rw [Nat.add_right_comm, Nat.add_assoc]