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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
x : α
⊢ Equiv.Perm.cycleOf g x ≠ 1 ↔ Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
Tactic:
rw [Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.mem_support,
      ne_eq, Equiv.Perm.cycleOf_eq_one_iff]
State after:
no goals