Theorem: Array.getElem_swap_ne (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ (swap x i j)[k] = x[k]
Tactic:
rw [getElem_swap, if_neg hjk, if_neg hik]
State after:
no goals