ι : Type ?u.347151
α : Type u_1
β : Type ?u.347157
f g : Perm α
x y✝ : α
hx : ↑f x ≠ x
hf : IsCycle f
y : α
x✝ : SameCycle f x y
hy : ↑f y = y
i : ℤ
hi : x = y
⊢ ↑f x = x
ι : Type ?u.347151
α : Type u_1
β : Type ?u.347157
f g : Perm α
x y✝ : α
hx : ↑f x ≠ x
hf : IsCycle f
y : α
x✝ : SameCycle f x y
hy : ↑f y = y
i : ℤ
hi : ↑(f ^ i) x = y
⊢ ↑f x = x
rw [← zpow_apply_eq_self_of_apply_eq_self hy i, (f ^ i).injective.eq_iff] at hi
no goals
ι : Type ?u.347151
α : Type u_1
β : Type ?u.347157
f g : Perm α
x y✝ : α
hx : ↑f x ≠ x
hf : IsCycle f
y : α
x✝ : SameCycle f x y
hy : ↑f y = y
i : ℤ
hi : x = y
⊢ ↑f x = x
rw [hi, hy]