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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k : Perm α
⊢ cycleFactorsFinset (k * g * k⁻¹) = Finset.map (Equiv.toEmbedding (MulAut.conj k).toEquiv) (cycleFactorsFinset g)
Tactic:
ext c
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ cycleFactorsFinset (k * g * k⁻¹) ↔
    c ∈ Finset.map (Equiv.toEmbedding (MulAut.conj k).toEquiv) (cycleFactorsFinset g)

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ cycleFactorsFinset (k * g * k⁻¹) ↔
    c ∈ Finset.map (Equiv.toEmbedding (MulAut.conj k).toEquiv) (cycleFactorsFinset g)
Tactic:
rw [Finset.mem_map_equiv]
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ cycleFactorsFinset (k * g * k⁻¹) ↔ (MulAut.conj k).symm c ∈ cycleFactorsFinset g

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

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ cycleFactorsFinset (k * g * k⁻¹) ↔ k * (MulAut.conj k).symm c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹)
Tactic:
apply iff_of_eq
State after:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ (c ∈ cycleFactorsFinset (k * g * k⁻¹)) = (k * (MulAut.conj k).symm c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹))

State before:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ (c ∈ cycleFactorsFinset (k * g * k⁻¹)) = (k * (MulAut.conj k).symm c * k⁻¹ ∈ cycleFactorsFinset (k * g * k⁻¹))
Tactic:
apply congr_arg₂ _ _
State after:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ cycleFactorsFinset (k * g * k⁻¹) = cycleFactorsFinset (k * g * k⁻¹)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (MulAut.conj k).symm c * k⁻¹

State before:
case a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ cycleFactorsFinset (k * g * k⁻¹) = cycleFactorsFinset (k * g * k⁻¹)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (MulAut.conj k).symm c * k⁻¹
Tactic:
rfl
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (MulAut.conj k).symm c * k⁻¹

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (MulAut.conj k).symm c * k⁻¹
Tactic:
simp only [MulEquiv.toEquiv_eq_coe, MulEquiv.coe_toEquiv_symm, MulAut.conj_symm_apply]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (k⁻¹ * c * k) * k⁻¹

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c = k * (k⁻¹ * c * k) * k⁻¹
Tactic:
group
State after:
no goals