English
Every cyclic permutation f has a unique cycle s together with a witness h that encodes f via s.formPerm h.
Русский
Каждая циклическая перестановка f есть ровно одно представление в виде пары циклического цикла s и свидетельства h, где s.formPerm h = f.
LaTeX
$$$$\exists! s:\mathrm{Cycle} α,\ exists h : s.Nodup \wedge s.formPerm h = f.$$$$
Lean4
theorem existsUnique_cycle {f : Perm α} (hf : IsCycle f) : ∃! s : Cycle α, ∃ h : s.Nodup, s.formPerm h = f :=
by
cases nonempty_fintype α
obtain ⟨x, hx, hy⟩ := id hf
refine ⟨f.toList x, ⟨nodup_toList f x, ?_⟩, ?_⟩
· simp [formPerm_toList, hf.cycleOf_eq hx]
· rintro ⟨l⟩ ⟨hn, rfl⟩
simp only [Cycle.mk_eq_coe, Cycle.coe_eq_coe, Cycle.formPerm_coe]
refine (toList_formPerm_isRotated_self _ ?_ hn _ ?_).symm
· contrapose! hx
suffices formPerm l = 1 by simp [this]
rw [formPerm_eq_one_iff _ hn]
exact Nat.le_of_lt_succ hx
· rw [← mem_toFinset]
refine support_formPerm_le l ?_
simpa using hx
