English
For a Nodup l with an explicit nonmembership condition, the set {x | formPerm l x ≠ x} equals l.toFinset.
Русский
Для Nodup l: множество {x | formPerm l x ≠ x} совпадает с l.toFinset.
LaTeX
$$$\{x \mid \mathrm{formPerm}\ l\ x \neq x\} = l^{\mathrm{toFinset}}$$$
Lean4
theorem support_formPerm_of_nodup' (l : List α) (h : Nodup l) (h' : ∀ x : α, l ≠ [x]) :
{x | formPerm l x ≠ x} = l.toFinset := by
apply _root_.le_antisymm
· exact support_formPerm_le' l
· intro x hx
simp only [Finset.mem_coe, mem_toFinset] at hx
obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx
rw [Set.mem_setOf_eq, formPerm_apply_getElem _ h]
intro H
rw [nodup_iff_injective_get, Function.Injective] at h
specialize h H
rcases (Nat.succ_le_of_lt hn).eq_or_lt with hn' | hn'
· simp only [← hn', Nat.mod_self] at h
refine not_exists.mpr h' ?_
rw [← length_eq_one_iff, ← hn', (Fin.mk.inj_iff.mp h).symm]
· simp [Nat.mod_eq_of_lt hn'] at h
