no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g σ : Perm α
⊢ support σ = ∅ ↔ σ = 1
simp_rw [Finset.ext_iff, mem_support, Finset.not_mem_empty, iff_false_iff, not_not,
  Equiv.Perm.ext_iff, one_apply]