Theorem: Equiv.Perm.mem_cycleFactorsFinset_conj' (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k • c ∈ cycleFactorsFinset (k • g) ↔ c ∈ cycleFactorsFinset g
Tactic:
simp only [ConjAct.smul_def]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ ConjAct.ofConjAct k * c * (ConjAct.ofConjAct k)⁻¹ ∈
      cycleFactorsFinset (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) ↔
    c ∈ cycleFactorsFinset g

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ ConjAct.ofConjAct k * c * (ConjAct.ofConjAct k)⁻¹ ∈
      cycleFactorsFinset (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹) ↔
    c ∈ cycleFactorsFinset g
Tactic:
apply Equiv.Perm.mem_cycleFactorsFinset_conj
State after:
no goals