simp only [get_set_ite]
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
⊢ (set (set x i a) j b)[k] = (set (set x j b) i a)[k]
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]