Theorem: Permutation.get_swap (Fifteen/Data/Permutation/Basic.lean)

State before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (Array.swap x.val (Fin.cast (_ : n = Array.size x.val) i) (Fin.cast (_ : n = Array.size x.val) j))[k] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
simp only [Array.getElem_swap, Fin.cast]
State after:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (if ↑j = k then x.val[↑i] else if ↑i = k then x.val[↑j] else x.val[k]) =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]

State before:
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (if ↑j = k then x.val[↑i] else if ↑i = k then x.val[↑j] else x.val[k]) =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
Tactic:
rfl
State after:
no goals