English
For any p and x, the list toList p x has no duplicates.
Русский
Для любых p и x список toList p x без повторов.
LaTeX
$$$$\mathrm{Nodup}(\mathrm{toList}\ p\ x).$$$$
Lean4
theorem nodup_toList (p : Perm α) (x : α) : Nodup (toList p x) :=
by
by_cases hx : p x = x
· rw [← notMem_support, ← toList_eq_nil_iff] at hx
simp [hx]
have hc : IsCycle (cycleOf p x) := isCycle_cycleOf p hx
rw [nodup_iff_injective_getElem]
intro ⟨n, hn⟩ ⟨m, hm⟩
rw [length_toList, ← hc.orderOf] at hm hn
rw [← cycleOf_apply_self, ← Ne, ← mem_support] at hx
simp only [Fin.mk.injEq]
rw [getElem_toList, getElem_toList, ← cycleOf_pow_apply_self p x n, ← cycleOf_pow_apply_self p x m]
rcases n with - | n <;> rcases m with - | m
· simp
· rw [← hc.support_pow_of_pos_of_lt_orderOf m.zero_lt_succ hm, mem_support, cycleOf_pow_apply_self] at hx
simp [hx.symm]
· rw [← hc.support_pow_of_pos_of_lt_orderOf n.zero_lt_succ hn, mem_support, cycleOf_pow_apply_self] at hx
simp [hx]
intro h
have hn' : ¬orderOf (p.cycleOf x) ∣ n.succ := Nat.not_dvd_of_pos_of_lt n.zero_lt_succ hn
have hm' : ¬orderOf (p.cycleOf x) ∣ m.succ := Nat.not_dvd_of_pos_of_lt m.zero_lt_succ hm
rw [← hc.support_pow_eq_iff] at hn' hm'
rw [← Nat.mod_eq_of_lt hn, ← Nat.mod_eq_of_lt hm, ← pow_inj_mod]
refine support_congr ?_ ?_
· rw [hm', hn']
· rw [hm']
intro y hy
obtain ⟨k, rfl⟩ := hc.exists_pow_eq (mem_support.mp hx) (mem_support.mp hy)
rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply, h, ← mul_apply, ← mul_apply,
(Commute.pow_pow_self _ _ _).eq]
