English
A list l is a permutation of replicate m a ++ replicate n b (with a ≠ b) precisely when l has exactly m copies of a, exactly n copies of b, and every element of l is either a or b.
Русский
Список l перестановочно эквивалентен конкатенации replicate m a и replicate n b при a ≠ b тогда, когда в l встречается ровно m копий a, ровно n копий b, и все элементы l принадлежат {a,b}.
LaTeX
$$$(a \\neq b) \\Rightarrow\\ l \\sim \\operatorname{replicate}(m,a) \\;\\mathrm{++}\\; \\operatorname{replicate}(n,b) \\iff \\#\\_l(a)=m \\land \\#\\_l(b)=n \\land l \\subseteq \\{a,b\\}$$$
Lean4
theorem perm_replicate_append_replicate [DecidableEq α] {l : List α} {a b : α} {m n : ℕ} (h : a ≠ b) :
l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b] :=
by
rw [perm_iff_count, ← Decidable.and_forall_ne a, ← Decidable.and_forall_ne b]
suffices l ⊆ [a, b] ↔ ∀ c, c ≠ b → c ≠ a → c ∉ l by
simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]
trans ∀ c, c ∈ l → c = b ∨ c = a
· simp [subset_def, or_comm]
· exact forall_congr' fun _ => by rw [← and_imp, ← not_or, not_imp_not]
