Theorem: mem_cycleAt_iff_le (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ y ∈ CycleAt π x ↔ ∃ b ≤ orderOf (π.cycleOf x) - 1, (π ^ b) x = y
Tactic:
simp_rw [mem_cycleAt_iff_lt, Nat.lt_iff_le_pred (orderOf_pos _)]
State after:
no goals