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