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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
a : α
⊢ a ∈ support c ↔ g a ∈ support c
Tactic:
apply Equiv.Perm.mem_support_of_commute
State after:
case hgc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
a : α
⊢ Commute g c

State before:
case hgc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ cycleFactorsFinset g
a : α
⊢ Commute g c
Tactic:
exact (Equiv.Perm.self_mem_cycle_factors_commute hc).symm
State after:
no goals