no goals
ι : Type ?u.41748
α : Type u_1
β : Type ?u.41754
f g : Perm α
p : α → Prop
x y z : α
x✝ : SameCycle f x y
i : ℤ
hi : ↑(f ^ i) x = y
⊢ ↑f x = x ↔ ↑f y = y
rw [← hi, ← mul_apply, ← zpow_one_add, add_comm, zpow_add_one, mul_apply,
  (f ^ i).injective.eq_iff]