simp [modify, modifyM, dite]
α : Type u_1
arr : Array α
f : α → α
n : Nat
⊢ size arr = size (modify arr n f)
α : Type u_1
arr : Array α
f : α → α
n : Nat
⊢ size arr =
    size
      (Id.run
        (Decidable.rec (fun h => arr) (fun h => set arr { val := n, isLt := h } (f arr[n])) (Nat.decLt n (size arr))))