Theorem: unswap_support (Bruhat/Word.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
a : α
⊢ a ∉ support (Equiv.swap a (f a) * f)
Tactic:
simp [support] at *
State after:
no goals