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

State before:
α✝ : Type u_1
x y : α✝
f g : Finperm α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ swapsOf Set.univ = swaps α
Tactic:
simp [swaps, swapsOf]
State after:
no goals