no goals
ι : Type ?u.2518697
α : Type u_1
β : Type ?u.2518703
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x y : α
hx : ↑f x ≠ x
⊢ y ∈ support (cycleOf f x) ↔ SameCycle f x y
rw [mem_support_cycleOf_iff, and_iff_left (mem_support.2 hx)]