Theorem: mem_cycleAt_iff_zpow (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ y ∈ CycleAt π x ↔ ∃ k, (π ^ k) x = y
Tactic:
simp_rw [mem_cycleAt_iff]
State after:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ π.SameCycle x y ↔ ∃ k, (π ^ k) x = y

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
y x : α
⊢ π.SameCycle x y ↔ ∃ k, (π ^ k) x = y
Tactic:
rfl
State after:
no goals