Theorem: Permutation.toFun_inv_toFun (Fifteen/Data/Permutation/Basic.lean)

State before:
n : Nat
x : Permutation n
i : Fin n
⊢ toFun (inv x) (toFun x i) = i
Tactic:
simp only [inv, toFun_ofFn]
State after:
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

State before:
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
Tactic:
exact Fin.invOfInj_left ..
State after:
no goals