Theorem: Finperm.mem_restrict_support (Bruhat/Finperm.lean)

State before:
α✝ : Type u_1
x y : α✝
f✝¹ g : Finperm α✝
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ f : Finperm α
⊢ f ∈ restrict ↑f.support
Tactic:
simp
State after:
no goals