Theorem: mem_cycleAtTo_iff (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y : α
a : ℕ
x : α
⊢ y ∈ CycleAtTo π a x ↔ ∃ b < a, (π ^ b) x = y
Tactic:
simp_rw [CycleAtTo, Finset.mem_image, Finset.mem_Iio]
State after:
no goals