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