no goals
cs cs' : List Char
i p : Nat
hp : i + utf8Len cs = p
⊢ utf8GetAux (cs ++ cs') { byteIdx := i } { byteIdx := p } = List.headD cs' default
match cs, cs' with
| [], [] => rfl
| [], c::cs' => simp [← hp, utf8GetAux]
| c::cs, cs' =>
  simp [utf8GetAux, -List.headD_eq_head?]; rw [if_neg]
  case hnc => rw [← hp]; apply Pos.ne_of_lt (Nat.lt_add_of_pos_right add_csize_pos)
  refine utf8GetAux_of_valid cs cs' ?_
  simpa [Nat.add_assoc, Nat.add_comm] using hp
no goals
cs cs' : List Char
i p : Nat
hp : i + utf8Len [] = p
⊢ utf8GetAux ([] ++ []) { byteIdx := i } { byteIdx := p } = List.headD [] default
rfl
no goals
cs cs'✝ : List Char
i p : Nat
c : Char
cs' : List Char
hp : i + utf8Len [] = p
⊢ utf8GetAux ([] ++ c :: cs') { byteIdx := i } { byteIdx := p } = List.headD (c :: cs') default
simp [← hp, utf8GetAux]
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ (if { byteIdx := i } = { byteIdx := p } then c else utf8GetAux (cs ++ cs') ({ byteIdx := i } + c) { byteIdx := p }) =
    List.headD cs' default
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ utf8GetAux (c :: cs ++ cs') { byteIdx := i } { byteIdx := p } = List.headD cs' default
simp [utf8GetAux, -List.headD_eq_head?]
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ utf8GetAux (cs ++ cs') ({ byteIdx := i } + c) { byteIdx := p } = List.headD cs' default

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

case hnc
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ ¬{ byteIdx := i } = { byteIdx := p }
case hnc => rw [← hp]; apply Pos.ne_of_lt (Nat.lt_add_of_pos_right add_csize_pos)
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ { byteIdx := i }.byteIdx + csize c + utf8Len cs = p
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ utf8GetAux (cs ++ cs') ({ byteIdx := i } + c) { byteIdx := p } = List.headD cs' default
refine utf8GetAux_of_valid cs cs' ?_
no goals
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ { byteIdx := i }.byteIdx + csize c + utf8Len cs = p
simpa [Nat.add_assoc, Nat.add_comm] using hp
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ ¬{ byteIdx := i } = { byteIdx := i + utf8Len (c :: cs) }
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ ¬{ byteIdx := i } = { byteIdx := p }
rw [← hp]
no goals
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ ¬{ byteIdx := i } = { byteIdx := i + utf8Len (c :: cs) }
apply Pos.ne_of_lt (Nat.lt_add_of_pos_right add_csize_pos)