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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x y : α
hx : Equiv.Perm.SameCycle g y x
hy : y ∈ Equiv.Perm.support ↑c
⊢ ↑c = Equiv.Perm.cycleOf g x
Tactic:
rw [Equiv.Perm.cycle_is_cycleOf hy c.prop, Equiv.Perm.SameCycle.cycleOf_eq hx]
State after:
no goals