Theorem: cycleMin_eq_cycleMin_apply (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
⊢ CycleMin π x = CycleMin π (π x)
Tactic:
simp_rw [cycleMin_def, cycleAt_apply_eq_cycleAt]
State after:
no goals