if hij : i.1 = j then
  cases hij; rw [if_pos rfl, get_set_eq]
else
  rw [get_set_ne (h:=hij), if_neg hij]
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
j : Nat
hj : j < n
⊢ (set x i v)[j] = if ↑i = j then v else x[j]
no goals