Theorem: Equiv.Perm.swap_eq_swap (Bruhat/Perm.lean)

State before:
α : Type u_1
x✝ y✝ : α
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
x x' y y' : α
⊢ swap x y = swap x' y' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
Tactic:
sorry
State after:
no goals