rewrite [(x.set i x[j.1]).get_set _ k hk]
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk✝ : k < size (set (set x i x[↑j]) ((_ : size x = size (set x i (get x j))) ▸ j) x[↑i])
hk : k < size (set x i x[↑j])
⊢ (if ↑((_ : size x = size (set x i (get x j))) ▸ j) = k then x[↑i] else (set x i x[↑j])[k]) =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]