English
For nodup lists l and l', formPerm l = formPerm l' iff either l ~r l' (rotation) or both lengths are ≤ 1.
Русский
Для неповторяющихся списков l и l' формулировка: formPerm l = formPerm l' тогда и только тогда, когда l и l' либо вращены друг к другу, либо обе длины не превышают 1.
LaTeX
$$$\forall {\alpha} [\DecidableEq \alpha],\ (l:\,\mathrm{List}\ \alpha),\ (l':\,\mathrm{List}\ \alpha),\ l.Nodup → l'.Nodup → (l.formPerm = l'.formPerm) \iff (l ~r l') ∨ l.length ≤ 1 ∧ l'.length ≤ 1$$$
Lean4
theorem formPerm_eq_formPerm_iff {l l' : List α} (hl : l.Nodup) (hl' : l'.Nodup) :
l.formPerm = l'.formPerm ↔ l ~r l' ∨ l.length ≤ 1 ∧ l'.length ≤ 1 :=
by
rcases l with (_ | ⟨x, _ | ⟨y, l⟩⟩)
· suffices l'.length ≤ 1 ↔ l' = nil ∨ l'.length ≤ 1 by
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff]
refine ⟨fun h => Or.inr h, ?_⟩
rintro (rfl | h)
· simp
· exact h
· suffices l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1 by
simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff, le_rfl]
refine ⟨fun h => Or.inr h, ?_⟩
rintro (h | h)
· simp [← h.perm.length_eq]
· exact h
· rcases l' with (_ | ⟨x', _ | ⟨y', l'⟩⟩)
· simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]
· simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]
· simp [-formPerm_cons_cons, formPerm_ext_iff hl hl']
