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

State before:
n : Nat
i j : Fin n
k : Nat
hk : k < n
⊢ (transpos i j)[k] = if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk }
Tactic:
simp only [transpos, get_swap, get_one]
State after:
no goals