rw [Array.modify_preserves_size]
α : Type ?u.26377
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ i < (a.modify i f).size
α : Type ?u.26377
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ i < a.size