English
For finite α, if x and y lie in the same f-cycle, there exist an i and bounds with i ≤ orderOf f such that (f^i) x = y, with i possibly negative or zero depending on formulation.
Русский
Для конечного множества α, если x и y лежат в одном цикле f, существует i с пределами, что i ≤ orderOf f и (f^i)x = y.
LaTeX
$$$[Finite\\ \\alpha]\\;\\forall f:\\mathrm{Equiv.Perm}(\\alpha),\\; \\forall x,y:\\alpha,\\mathrm{SameCycle}(f,x,y) \\Rightarrow \\exists i\\le\\mathrm{orderOf}(f), (f^i)x = y.$$$
Lean4
theorem exists_pow_eq' [Finite α] : SameCycle f x y → ∃ i < orderOf f, (f ^ i) x = y :=
by
rintro ⟨k, rfl⟩
use (k % orderOf f).natAbs
have h₀ := Int.natCast_pos.mpr (orderOf_pos f)
have h₁ := Int.emod_nonneg k h₀.ne'
rw [← zpow_natCast, Int.natAbs_of_nonneg h₁, zpow_mod_orderOf]
refine ⟨?_, by rfl⟩
rw [← Int.ofNat_lt, Int.natAbs_of_nonneg h₁]
exact Int.emod_lt_of_pos _ h₀
