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

State before:
α : Type u_1
x y : α
f✝ g f : Finperm α
h : f.support = ∅
⊢ f.support = refl.support
Tactic:
simp [h]
State after:
no goals

State before:
α : Type u_1
x y : α
f✝ g f : Finperm α
h : f.support = ∅
⊢ ∀ i ∈ f.support, f i = refl i
Tactic:
simp [h]
State after:
no goals