English
If y appears in toList p x, then the successor along the cycle yields p y.
Русский
Если y встречается в toList p x, то следующий по списку после y равен p y.
LaTeX
$$$$\text{If } y \in toList\ p\ x,\ \text{then }\ \text{next}(\mathrm{toList}\ p\ x)\ y\ _{\text{hy}} = p\ y.$$$$
Lean4
theorem next_toList_eq_apply (p : Perm α) (x y : α) (hy : y ∈ toList p x) : next (toList p x) y hy = p y :=
by
rw [mem_toList_iff] at hy
obtain ⟨k, hk, hk'⟩ := hy.left.exists_pow_eq_of_mem_support hy.right
rw [← getElem_toList p x k (by simpa using hk)] at hk'
simp_rw [← hk']
rw [next_getElem _ (nodup_toList _ _), getElem_toList, getElem_toList, ← mul_apply, ← pow_succ']
simp_rw [length_toList]
rw [← pow_mod_orderOf_cycleOf_apply p (k + 1), IsCycle.orderOf]
exact isCycle_cycleOf _ (mem_support.mp hy.right)
