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

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

State before:
case h
α✝ : Type u_1
x y : α✝
f : Perm α✝
α : Type u_2
x✝ : α
⊢ x✝ ∈ support' 1 ↔ x✝ ∈ ∅
Tactic:
simp
State after:
no goals