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

State before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hxy : x ≠ y
⊢ (swap x y).support = {x, y}
Tactic:
simp [swap, hxy]
State after:
no goals