Theorem: Equiv.Perm.Basis.eq_cycleOf (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ↑c = Equiv.Perm.cycleOf g ((g ^ i) (a c))
Tactic:
rw [Equiv.Perm.cycleOf_self_apply_zpow]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ↑c = Equiv.Perm.cycleOf g (a c)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
i : ℤ
⊢ ↑c = Equiv.Perm.cycleOf g (a c)
Tactic:
rw [a.cycleOf_eq]
State after:
no goals