no goals
cs cs' : List Char
c : Char
i p : Nat
hp : i + (utf8Len cs + csize c) = p
⊢ utf8PrevAux (cs ++ c :: cs') { byteIdx := i } { byteIdx := p } = { byteIdx := i + utf8Len cs }
match cs with
| [] => simp [utf8PrevAux, ← hp, Pos.addChar_eq]
| c'::cs =>
  simp [← hp, utf8PrevAux, Pos.addChar_eq]; rw [if_neg]
  case hnc => rw [Pos.ext_iff, Nat.add_right_comm, Nat.add_left_comm]; apply ne_add_csize_add_self
  refine (utf8PrevAux_of_valid (by simp [Nat.add_assoc, Nat.add_left_comm])).trans ?_
  simp [Nat.add_assoc, Nat.add_comm]
no goals
cs cs' : List Char
c : Char
i p : Nat
hp : i + (utf8Len [] + csize c) = p
⊢ utf8PrevAux ([] ++ c :: cs') { byteIdx := i } { byteIdx := p } = { byteIdx := i + utf8Len [] }
simp [utf8PrevAux, ← hp, Pos.addChar_eq]
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ (if { byteIdx := i + csize c' } = { byteIdx := i + (utf8Len cs + csize c' + csize c) } then { byteIdx := i }
    else
      utf8PrevAux (cs ++ c :: cs') { byteIdx := i + csize c' } { byteIdx := i + (utf8Len cs + csize c' + csize c) }) =
    { byteIdx := i + (utf8Len cs + csize c') }
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ utf8PrevAux (c' :: cs ++ c :: cs') { byteIdx := i } { byteIdx := p } = { byteIdx := i + utf8Len (c' :: cs) }
simp [← hp, utf8PrevAux, Pos.addChar_eq]
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ utf8PrevAux (cs ++ c :: cs') { byteIdx := i + csize c' } { byteIdx := i + (utf8Len cs + csize c' + csize c) } =
    { byteIdx := i + (utf8Len cs + csize c') }

case hnc
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ ¬{ byteIdx := i + csize c' } = { byteIdx := i + (utf8Len cs + csize c' + csize c) }
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ (if { byteIdx := i + csize c' } = { byteIdx := i + (utf8Len cs + csize c' + csize c) } then { byteIdx := i }
    else
      utf8PrevAux (cs ++ c :: cs') { byteIdx := i + csize c' } { byteIdx := i + (utf8Len cs + csize c' + csize c) }) =
    { byteIdx := i + (utf8Len cs + csize c') }
rw [if_neg]
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ utf8PrevAux (cs ++ c :: cs') { byteIdx := i + csize c' } { byteIdx := i + (utf8Len cs + csize c' + csize c) } =
    { byteIdx := i + (utf8Len cs + csize c') }
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ utf8PrevAux (cs ++ c :: cs') { byteIdx := i + csize c' } { byteIdx := i + (utf8Len cs + csize c' + csize c) } =
    { byteIdx := i + (utf8Len cs + csize c') }

case hnc
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ ¬{ byteIdx := i + csize c' } = { byteIdx := i + (utf8Len cs + csize c' + csize c) }
case hnc => rw [Pos.ext_iff, Nat.add_right_comm, Nat.add_left_comm]; apply ne_add_csize_add_self
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ { byteIdx := i + csize c' + utf8Len cs } = { byteIdx := i + (utf8Len cs + csize c') }
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ utf8PrevAux (cs ++ c :: cs') { byteIdx := i + csize c' } { byteIdx := i + (utf8Len cs + csize c' + csize c) } =
    { byteIdx := i + (utf8Len cs + csize c') }
refine (utf8PrevAux_of_valid (by simp [Nat.add_assoc, Nat.add_left_comm])).trans ?_
no goals
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ { byteIdx := i + csize c' + utf8Len cs } = { byteIdx := i + (utf8Len cs + csize c') }
simp [Nat.add_assoc, Nat.add_comm]
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ ¬{ byteIdx := i + csize c' }.byteIdx = { byteIdx := utf8Len cs + csize c + (i + csize c') }.byteIdx
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ ¬{ byteIdx := i + csize c' } = { byteIdx := i + (utf8Len cs + csize c' + csize c) }
rw [Pos.ext_iff, Nat.add_right_comm, Nat.add_left_comm]
no goals
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ ¬{ byteIdx := i + csize c' }.byteIdx = { byteIdx := utf8Len cs + csize c + (i + csize c') }.byteIdx
apply ne_add_csize_add_self
no goals
cs✝ cs' : List Char
c : Char
i p : Nat
c' : Char
cs : List Char
hp : i + (utf8Len (c' :: cs) + csize c) = p
⊢ i + csize c' + (utf8Len cs + csize c) = i + (utf8Len cs + csize c' + csize c)
simp [Nat.add_assoc, Nat.add_left_comm]