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

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

State before:
case h
n : Nat
x : Permutation n
i : Fin n
⊢ toFun (x * inv 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 x ∘ toFun (inv x)) i = id i

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