Theorem: cycleMin_eq_min_cycleAtTo_ge (Controlbits/Cycles.lean)

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