Theorem: Finperm.cl_swapsAt_eq' (Bruhat/Finperm.lean)

State before:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
hxt : x ∈ t
⊢ Subgroup.closure (swapsAt x t) = restrict t
Tactic:
rw [cl_swapsAt_eq, Set.insert_eq_of_mem hxt]
State after:
no goals