Theorem: cycleAt_eq_cycleAtTo_orderOf_cycleOf (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAt π x = CycleAtTo π (orderOf (π.cycleOf x)) x
Tactic:
simp_rw [Finset.ext_iff, mem_cycleAtTo_iff, mem_cycleAt_iff_lt, implies_true]
State after:
no goals