Theorem: Equiv.Perm.not_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