Theorem: SizedArray.get_swap (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
k : Nat
hk : k < n
⊢ (swap x i j)[k] = if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
rw [swap_eq, get_set_ite, get_set_ite]
State after:
no goals