rw [Array.modify_preserves_size]
α : Type ?u.27672
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ j < (a.modify i f).size
α : Type ?u.27672
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ j < a.size