Theorem: Equiv.Perm.support'_inv (Bruhat/Perm.lean)

State before:
α : Type u_1
x y : α
f✝ f : Perm α
⊢ support' f⁻¹ = support' f
Tactic:
ext x
State after:
case h
α : Type u_1
x✝ y : α
f✝ f : Perm α
x : α
⊢ x ∈ support' f⁻¹ ↔ x ∈ support' f

State before:
case h
α : Type u_1
x✝ y : α
f✝ f : Perm α
x : α
⊢ x ∈ support' f⁻¹ ↔ x ∈ support' f
Tactic:
rw [mem_support', ne_eq, mem_support', inv_eq_iff_eq, eq_comm]
State after:
no goals