simp only [if_neg hjk, if_pos]
case refl
n : Nat
x : Permutation n
i j : Fin n
hk : ↑i < n
hjk : ¬↑j = ↑i
⊢ x[↑(if ↑j = ↑i then i else if ↑i = ↑i then j else { val := ↑i, isLt := hk })] =
    if ↑j = ↑i then x[↑i] else if ↑i = ↑i then x[↑j] else x[↑i]
no goals