Theorem: cycleMin_eq_min_cycleAtTo (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
⊢ CycleMin π x = (CycleAtTo π (orderOf (π.cycleOf x)) x).min' ⋯
Tactic:
simp_rw [cycleMin_def, cycleAt_eq_cycleAtTo_orderOf_cycleOf]
State after:
no goals