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

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ (swap x i j)[↑i] = x[↑j]
Tactic:
rw [swap_comm, get_swap_second]
State after:
no goals