no goals
ι : Type ?u.2369326
α : Type u_1
β : Type ?u.2369332
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
⊢ ↑(cycleOf f x) (↑f x) = ↑f (↑f x)
convert cycleOf_apply_apply_pow_self f x 1 using 1