Theorem: Equiv.Perm.disjoint_iff_support_disjoint (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
⊢ Disjoint f g ↔ _root_.Disjoint (support f) (support g)
Tactic:
simp only [Equiv.Perm.disjoint_iff_eq_or_eq,
  Finset.disjoint_iff_inter_eq_empty, ← Equiv.Perm.not_mem_support,
  ← Finset.mem_compl, ← Finset.mem_union, ← Finset.compl_inter,
  ← Finset.compl_eq_univ_iff, ← Finset.eq_univ_iff_forall]
State after:
no goals