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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
⊢ cycleFactorsFinset (k • g) = k • cycleFactorsFinset g
Tactic:
ext c
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ c ∈ cycleFactorsFinset (k • g) ↔ c ∈ k • cycleFactorsFinset g

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ c ∈ cycleFactorsFinset (k • g) ↔ c ∈ k • cycleFactorsFinset g
Tactic:
rw [← Equiv.Perm.mem_cycleFactorsFinset_conj' k⁻¹ (k • g) c]
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ cycleFactorsFinset (k⁻¹ • k • g) ↔ c ∈ k • cycleFactorsFinset g

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

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ cycleFactorsFinset g ↔ c ∈ k • cycleFactorsFinset g
Tactic:
exact Finset.inv_smul_mem_iff
State after:
no goals