English
For a Nodup l and x ∈ l, formPerm l x = x iff the length of l is at most 1.
Русский
Для Nodup l и x ∈ l, formPerm l x = x тогда и только тогда, когда длина l не превосходит 1.
LaTeX
$$$\forall {\alpha} [\DecidableEq \alpha],\ (l:\,\mathrm{List}\ \alpha),\ l.Nodup \rightarrow \forall x:\,\alpha,\ (x \in l) \rightarrow (\mathrm{formPerm}\ l\ x = x \iff \mathrm{length}\ l \le 1)$$$
Lean4
theorem formPerm_apply_mem_eq_self_iff (hl : Nodup l) (x : α) (hx : x ∈ l) : formPerm l x = x ↔ length l ≤ 1 :=
by
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
rw [formPerm_apply_getElem _ hl k hk, hl.getElem_inj_iff]
cases hn : l.length
· exact absurd k.zero_le (hk.trans_le hn.le).not_ge
· rw [hn] at hk
rcases (Nat.le_of_lt_succ hk).eq_or_lt with hk' | hk'
· simp [← hk', eq_comm]
· simpa [Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.succ_lt_succ_iff] using (k.zero_le.trans_lt hk').ne.symm
