simp [insertSorted', *]
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
arr : Array α
isLt : Nat.zero < Array.size arr
hLen : Array.size arr = len
⊢ Array.size (insertSorted' arr { val := Nat.zero, isLt := isLt }) = len
no goals