Theorem: Subarray.getElem_swap_right (Algdata/Data/Array/Subarray.lean)

State before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (swap x i j)[↑j] = x[↑i]
Tactic:
rewrite [getElem_swap]
State after:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (if ↑j = ↑j then x[↑i] else if ↑i = ↑j then x[↑j] else x[↑j]) = x[↑i]

State before:
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (if ↑j = ↑j then x[↑i] else if ↑i = ↑j then x[↑j] else x[↑j]) = x[↑i]
Tactic:
rw [if_pos rfl]
State after:
no goals