English
If s is a noduplicate list, then all permutations of s are pairwise distinct.
Русский
Если список s без повторов, то его перестановки попарно различны.
LaTeX
$$$\operatorname{Nodup}(s) \rightarrow \operatorname{Nodup}(s.permutations)$$$
Lean4
theorem nodup_permutations (s : List α) (hs : Nodup s) : Nodup s.permutations :=
by
rw [(permutations_perm_permutations' s).nodup_iff]
induction hs with
| nil => simp
| @cons x l h h' IH =>
rw [permutations']
rw [nodup_flatMap]
constructor
· intro ys hy
rw [mem_permutations'] at hy
rw [nodup_permutations'Aux_iff, hy.mem_iff]
exact fun H => h x H rfl
· refine IH.pairwise_of_forall_ne fun as ha bs hb H => ?_
rw [Function.onFun, disjoint_iff_ne]
rintro a ha' b hb' rfl
obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'
obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'
rw [mem_permutations'] at ha hb
have hl : as.length = bs.length := (ha.trans hb.symm).length_eq
simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm
rw [get_permutations'Aux] at hn' hm'
have hx : (as.insertIdx n x)[m]'(by rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]) = x := by
simp [hn', ← hm']
have hx' : (bs.insertIdx m x)[n]'(by rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]) = x := by
simp [hm', ← hn']
rcases lt_trichotomy n m with (ht | ht | ht)
· suffices x ∈ bs by exact h x (hb.subset this) rfl
rw [← hx', getElem_insertIdx_of_lt ht]
exact getElem_mem _
· simp only [ht] at hm' hn'
rw [← hm'] at hn'
exact H (insertIdx_injective _ _ hn')
· suffices x ∈ as by exact h x (ha.subset this) rfl
rw [← hx, getElem_insertIdx_of_lt ht]
exact getElem_mem _
