by_cases h : i < arr.data.size <;> simp [h]
arr : ByteArray
i : Nat
u : UInt8
⊢ Array.size (if h : i < Array.size arr.data then Array.set arr.data { val := i, isLt := h } u else arr.data) =
    Array.size arr.data
no goals