simp only [Array.modify, Array.modifyM, Id.bind_eq, Id.pure_eq, Id.run]
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ (a.modify i f).size = a.size
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ Array.size (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a) = a.size