English
Nodup (permutations'Aux x s) if and only if x ∉ s.
Русский
Nodup (permutations'Aux x s) тогда и только тогда, когда x ∉ s.
LaTeX
$$$\operatorname{Nodup}(\operatorname{permutations'Aux} x s) \iff x \notin s$$$
Lean4
theorem nodup_permutations'Aux_iff {s : List α} {x : α} : Nodup (permutations'Aux x s) ↔ x ∉ s :=
by
refine ⟨fun h H ↦ ?_, nodup_permutations'Aux_of_notMem _ _⟩
obtain ⟨⟨k, hk⟩, hk'⟩ := get_of_mem H
rw [nodup_iff_injective_get] at h
apply k.succ_ne_self.symm
have kl : k < (permutations'Aux x s).length := by simpa [Nat.lt_succ_iff] using hk.le
have k1l : k + 1 < (permutations'Aux x s).length := by simpa using hk
rw [← @Fin.mk.inj_iff _ _ _ kl k1l]; apply h
rw [get_permutations'Aux, get_permutations'Aux]
have hl : length (s.insertIdx k x) = length (s.insertIdx (k + 1) x) := by
rw [length_insertIdx_of_le_length hk.le, length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)]
exact ext_get hl fun n hn hn' => by grind
