simp [swap, getElem_eq_data_get, List.get_set, this]
α : Type u
as : Array α
i j : Fin (size as)
k : Nat
hk : k < size (swap as i j)
this : ∀ {m n : Nat} (h : m = n) (i : Fin m), (h ▸ i).val = i.val
⊢ (swap as i j)[k] = if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]
no goals