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

State before:
n : Nat
x : Permutation n
⊢ toFun (inv x * x) = toFun 1
Tactic:
funext i
State after:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ toFun (inv x * x) i = toFun 1 i

State before:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ toFun (inv x * x) i = toFun 1 i
Tactic:
simp only [toFun_mul, toFun_one]
State after:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ (toFun (inv x) ∘ toFun x) i = id i

State before:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ (toFun (inv x) ∘ toFun x) i = id i
Tactic:
exact toFun_inv_toFun x i
State after:
no goals