English
If l is nodal (no duplicates), then permsOfList(l) contains no duplicates.
Русский
Если список l без повторов, то permsOfList(l) также без повторов.
LaTeX
$$$l.Nodup \\Rightarrow (\\mathrm{permsOfList}(l)).Nodup$$$
Lean4
theorem nodup_permsOfList : ∀ {l : List α}, l.Nodup → (permsOfList l).Nodup
| [], _ => by simp [permsOfList]
| a :: l, hl => by
have hl' : l.Nodup := hl.of_cons
have hln' : (permsOfList l).Nodup := nodup_permsOfList hl'
have hmeml : ∀ {f : Perm α}, f ∈ permsOfList l → f a = a := fun {f} hf =>
not_not.1 (mt (mem_of_mem_permsOfList hf) (nodup_cons.1 hl).1)
rw [permsOfList, List.nodup_append', List.nodup_flatMap, pairwise_iff_getElem]
refine ⟨?_, ⟨⟨?_, ?_⟩, ?_⟩⟩
· exact hln'
· exact fun _ _ => hln'.map fun _ _ => mul_left_cancel
· intro i j hi hj hij x hx₁ hx₂
let ⟨f, hf⟩ := List.mem_map.1 hx₁
let ⟨g, hg⟩ := List.mem_map.1 hx₂
have hix : x a = l[i] := by rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
have hiy : x a = l[j] := by rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
have hieqj : i = j := hl'.getElem_inj_iff.1 (hix.symm.trans hiy)
exact absurd hieqj (_root_.ne_of_lt hij)
· intro f hf₁ hf₂
let ⟨x, hx, hx'⟩ := List.mem_flatMap.1 hf₂
let ⟨g, hg⟩ := List.mem_map.1 hx'
have hgxa : g⁻¹ x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
have hxa : x ≠ a := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)
exact (List.nodup_cons.1 hl).1 <| hgxa ▸ mem_of_mem_permsOfList hg.1 (by rwa [apply_inv_self, hgxa])
