English
There exists an element a in s with f a = b and (s.erase a).map f = t if and only if map f s = b ::ₘ t (i.e., f maps some a to b and the remaining elements map to t).
Русский
Существует элемент a в s такой, что f a = b и (s.erase a).map f = t тогда и только тогда map f s = b ::ₘ t (то есть образом f соответствующий элемент a даёт b, а оставшиеся элементы дают t).
LaTeX
$$$$ \\big(\\exists a \\in s, f a = b \\land (s.erase a).map f = t\\big) \\iff \\operatorname{map} f s = b ::ₘ t $$$$
Lean4
theorem map_eq_cons [DecidableEq α] (f : α → β) (s : Multiset α) (t : Multiset β) (b : β) :
(∃ a ∈ s, f a = b ∧ (s.erase a).map f = t) ↔ s.map f = b ::ₘ t :=
by
constructor
· rintro ⟨a, ha, rfl, rfl⟩
rw [← map_cons, Multiset.cons_erase ha]
· intro h
have : b ∈ s.map f := by
rw [h]
exact mem_cons_self _ _
obtain ⟨a, h1, rfl⟩ := mem_map.mp this
obtain ⟨u, rfl⟩ := exists_cons_of_mem h1
rw [map_cons, cons_inj_right] at h
refine ⟨a, mem_cons_self _ _, rfl, ?_⟩
rw [Multiset.erase_cons_head, h]
-- The simpNF linter says that the LHS can be simplified via `Multiset.mem_map`.
-- However this is a higher priority lemma.
-- It seems the side condition `H` is not applied by `simpNF`.
-- https://github.com/leanprover/std4/issues/207
