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

State before:
α✝ : Type u_1
x y : α✝
f g : Finperm α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ Subgroup.closure (swaps α) = ⊤
Tactic:
rw [← swapsOf_univ_eq, ← restrict_univ]
State after:
α✝ : Type u_1
x y : α✝
f g : Finperm α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ Subgroup.closure (swapsOf Set.univ) = restrict Set.univ

State before:
α✝ : Type u_1
x y : α✝
f g : Finperm α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ Subgroup.closure (swapsOf Set.univ) = restrict Set.univ
Tactic:
exact cl_swapsOf_eq _
State after:
no goals