if hjk : j.1 = k then
  cases hjk; simp only [if_pos]
else if hik : i.1 = k then
  cases hik; simp only [if_neg hjk, if_pos]
else
  simp only [if_neg hjk, if_neg hik]
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ x[↑(if ↑j = k then i else if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]
no goals