Theorem: cycleAt_of_fixed (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
h : Function.IsFixedPt (⇑π) x
⊢ CycleAt π x = {x}
Tactic:
simp_rw [Finset.ext_iff, mem_cycleAt_iff_zpow, mem_singleton, (fun k => (h.perm_zpow k).eq),
exists_const, eq_comm, implies_true]
State after:
no goals