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

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

State before:
n : Nat
x : Permutation n
i : Fin n
⊢ toFun x (Fin.invOfInj (toFun x) (_ : ∀ (i j : Fin n), toFun x i = toFun x j → i = j) i) = i
Tactic:
exact Fin.invOfInj_right ..
State after:
no goals