if hik : i.1 = k then
  cases hik; simp only [if_pos]
else
  have : x[i.1].1 ≠ x[k].1 :=
    fun h => hik <| x.get_inj _ _ (Fin.eq_of_val_eq h)
  simp only [hik, this, if_neg]
n : Nat
i j : Fin n
x : Permutation n
k : Nat
hk : k < n
hjk : ¬↑j = k
this : ↑x[↑j] ≠ ↑x[k]
⊢ x[↑(if ↑i = k then j else { val := k, isLt := hk })] =
    if ↑x[↑i] = ↑x[k] then x[↑j] else { val := ↑x[k], isLt := (_ : ↑x[k] < n) }
no goals