simp only [inv, toFun_ofFn]
n : Nat
x : Permutation n
i : Fin n
⊢ toFun (inv x) (toFun x i) = i
n : Nat
x : Permutation n
i : Fin n
⊢ Fin.invOfInj (toFun x) (_ : ∀ (i j : Fin n), toFun x i = toFun x j → i = j) (toFun x i) = i