Theorem: ByteArray.set!_size (YatimaStdLib/ByteArray.lean)

State before:
arr : ByteArray
i : Nat
u : UInt8
⊢ size (set! arr i u) = size arr
Tactic:
simp [size, set!, Array.set!, Array.setD]
State after:
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

State before:
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
Tactic:
by_cases h : i < arr.data.size <;> simp [h]
State after:
no goals