English
Two cons multisets are equal if and only if either the heads are equal and the tails are equal, or the heads are different and there exists a common tail with swapped heads.
Русский
Две мультиконструкции вида a ::ₘ as и b ::ₘ bs равны тогда, когда либо a = b и as = bs, либо a ≠ b и существует cs such that as = b ::ₘ cs и bs = a ::ₘ cs.
LaTeX
$$$a ::ₘ as = b ::ₘ bs \\iff (a = b \\land as = bs) \\lor (a \\neq b \\land \\exists cs, as = b ::ₘ cs \\land bs = a ::ₘ cs)$$$
Lean4
theorem cons_eq_cons {a b : α} {as bs : Multiset α} :
a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs :=
by
haveI : DecidableEq α := Classical.decEq α
constructor
· intro eq
by_cases h : a = b
· subst h
simp_all
· have : a ∈ b ::ₘ bs := eq ▸ mem_cons_self _ _
have : a ∈ bs := by simpa [h]
rcases exists_cons_of_mem this with ⟨cs, hcs⟩
simp only [h, hcs, false_and, ne_eq, not_false_eq_true, cons_inj_right, exists_eq_right', true_and, false_or]
have : a ::ₘ as = b ::ₘ a ::ₘ cs := by simp [eq, hcs]
have : a ::ₘ as = a ::ₘ b ::ₘ cs := by rwa [cons_swap]
simpa using this
· intro h
rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)
· simp [*]
· simp [*, cons_swap a b]
