no goals
c' : Char
cs cs' : List Char
i p : Nat
hp : i + utf8Len [] = p
⊢ utf8SetAux c' ([] ++ []) { byteIdx := i } { byteIdx := p } = [] ++ List.modifyHead (fun x => c') []
rfl
no goals
c' : Char
cs cs'✝ : List Char
i p : Nat
c : Char
cs' : List Char
hp : i + utf8Len [] = p
⊢ utf8SetAux c' ([] ++ c :: cs') { byteIdx := i } { byteIdx := p } = [] ++ List.modifyHead (fun x => c') (c :: cs')
simp [← hp, utf8SetAux]
c' : Char
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' :: (cs ++ cs')
    else c :: utf8SetAux c' (cs ++ cs') ({ byteIdx := i } + c) { byteIdx := p }) =
    c ::
      (cs ++
        match cs' with
        | [] => []
        | a :: l => c' :: l)
c' : Char
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ utf8SetAux c' (c :: cs ++ cs') { byteIdx := i } { byteIdx := p } = c :: cs ++ List.modifyHead (fun x => c') cs'
simp [utf8SetAux]
c' : Char
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ c :: utf8SetAux c' (cs ++ cs') ({ byteIdx := i } + c) { byteIdx := p } =
    c ::
      (cs ++
        match cs' with
        | [] => []
        | a :: l => c' :: l)

case hnc
c' : Char
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ ¬{ byteIdx := i } = { byteIdx := p }
c' : Char
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' :: (cs ++ cs')
    else c :: utf8SetAux c' (cs ++ cs') ({ byteIdx := i } + c) { byteIdx := p }) =
    c ::
      (cs ++
        match cs' with
        | [] => []
        | a :: l => c' :: l)
rw [if_neg]
c' : Char
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ c :: utf8SetAux c' (cs ++ cs') ({ byteIdx := i } + c) { byteIdx := p } =
    c ::
      (cs ++
        match cs' with
        | [] => []
        | a :: l => c' :: l)
c' : Char
cs✝ cs'✝ : List Char
i p : Nat
c : Char
cs cs' : List Char
hp : i + utf8Len (c :: cs) = p
⊢ c :: utf8SetAux c' (cs ++ cs') ({ byteIdx := i } + c) { byteIdx := p } =
    c ::
      (cs ++
        match cs' with
        | [] => []
        | a :: l => c' :: l)

case hnc
c' : Char
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)
no goals
c' : Char
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
c' : Char
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) }
c' : Char
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
c' : Char
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)