Theorem: Equiv.Perm.mem_support' (Bruhat/Perm.lean)

State before:
α : Type u_1
x y : α
f✝ f : Perm α
⊢ x ∈ support' f ↔ f x ≠ x
Tactic:
simp [support']
State after:
no goals