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