Theorem: cycleAt_card_eq_orderOf_cycleOf (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ orderOf (π.cycleOf x) = (CycleAt π x).card
Tactic:
simp_rw [cycleAt_eq_cycleAtTo_orderOf_cycleOf, cycleAtTo_card_eq_of_le_orderOf_cycleOf (le_refl _)]
State after:
no goals