no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ Disjoint f g ↔ _root_.Disjoint (support f) (support g)
simp [disjoint_iff_eq_or_eq, disjoint_iff, disjoint_iff, Finset.ext_iff, not_and_or,
  imp_iff_not_or]