Theorem: Finperm.symm_symm (Bruhat/Finperm.lean)

State before:
α : Type u_1
x y : α
f✝ g f : Finperm α
⊢ f.symm.symm = f
Tactic:
apply coe_inj
State after:
case h
α : Type u_1
x y : α
f✝ g f : Finperm α
⊢ f.symm.symm.toPerm = f.toPerm

State before:
case h
α : Type u_1
x y : α
f✝ g f : Finperm α
⊢ f.symm.symm.toPerm = f.toPerm
Tactic:
simp
State after:
no goals