Theorem: mem_cycleAt_iff (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ y ∈ CycleAt π x ↔ π.SameCycle x y
Tactic:
simp_rw [CycleAt, mem_filter, mem_univ, true_and]
State after:
no goals