f : Char → Char
cs cs' : List Char
⊢ { data := cs ++ List.modifyHead (fun x => f (List.headD cs' default)) cs' } = { data := cs ++ List.modifyHead f cs' }
f : Char → Char
cs cs' : List Char
⊢ modify { data := cs ++ cs' } { byteIdx := utf8Len cs } f = { data := cs ++ List.modifyHead f cs' }
rw [modify, set_of_valid, get_of_valid]
no goals
f : Char → Char
cs cs' : List Char
⊢ { data := cs ++ List.modifyHead (fun x => f (List.headD cs' default)) cs' } = { data := cs ++ List.modifyHead f cs' }
cases cs' <;> rfl