Theorem: cycleAtTo_one (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
π : Perm α
inst✝ : Fintype α
x : α
⊢ CycleAtTo π 1 x = {x}
Tactic:
simp_rw [Finset.ext_iff, mem_cycleAtTo_iff, Nat.lt_one_iff, exists_eq_left, pow_zero,
  Perm.one_apply, mem_singleton, eq_comm, implies_true]
State after:
no goals