ι : Type ?u.377965
α : Type u_1
β : Type ?u.377971
f g : Perm α
x y : α
inst✝ : Finite α
hf : IsCycle f
hx : ↑f x ≠ x
hy : ↑f y ≠ y
n : ℤ
hn : ↑(f ^ n) x = y
⊢ ∃ i, ↑(f ^ i) x = y
ι : Type ?u.377965
α : Type u_1
β : Type ?u.377971
f g : Perm α
x y : α
inst✝ : Finite α
hf : IsCycle f
hx : ↑f x ≠ x
hy : ↑f y ≠ y
⊢ ∃ i, ↑(f ^ i) x = y
let ⟨n, hn⟩ := hf.exists_zpow_eq hx hy
no goals
ι : Type ?u.377965
α : Type u_1
β : Type ?u.377971
f g : Perm α
x y : α
inst✝ : Finite α
hf : IsCycle f
hx : ↑f x ≠ x
hy : ↑f y ≠ y
n : ℤ
hn : ↑(f ^ n) x = y
⊢ ∃ i, ↑(f ^ i) x = y
classical exact
    ⟨(n % orderOf f).toNat, by
      {have := n.emod_nonneg (Int.coe_nat_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
       rwa [← zpow_ofNat, Int.toNat_of_nonneg this, ← zpow_eq_mod_orderOf]}⟩
no goals
ι : Type ?u.377965
α : Type u_1
β : Type ?u.377971
f g : Perm α
x y : α
inst✝ : Finite α
hf : IsCycle f
hx : ↑f x ≠ x
hy : ↑f y ≠ y
n : ℤ
hn : ↑(f ^ n) x = y
⊢ ∃ i, ↑(f ^ i) x = y
exact
⟨(n % orderOf f).toNat, by
{have := n.emod_nonneg (Int.coe_nat_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
rwa [← zpow_ofNat, Int.toNat_of_nonneg this, ← zpow_eq_mod_orderOf]}⟩