Theorem: Equiv.Perm.IsCycle.nonempty_support (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
⊢ (support g).Nonempty
Tactic:
rw [Finset.nonempty_iff_ne_empty, Ne.def, Equiv.Perm.support_eq_empty_iff]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
⊢ ¬g = 1

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
⊢ ¬g = 1
Tactic:
exact Equiv.Perm.IsCycle.ne_one hg
State after:
no goals