English
The lemma relates the attach of a ndinsert to the attach of s via a constructive mapping induced by a membership predicate.
Русский
Лемма связывает прикрепление ndinsert с прикреплением s через отображение, порождаемое предикатом принадлежности.
LaTeX
$$$ (s.ndinsert a).attach = ndinsert \\langle a, mem\\_ndinsert\\_self a s \\rangle (s.attach.map (\\lambda p, \\langle p.1, mem\\_ndinsert\\_of\\_mem p.2\\rangle)) $$$
Lean4
theorem attach_ndinsert (a : α) (s : Multiset α) :
(s.ndinsert a).attach =
ndinsert ⟨a, mem_ndinsert_self a s⟩ (s.attach.map fun p => ⟨p.1, mem_ndinsert_of_mem p.2⟩) :=
have eq :
∀ h : ∀ p : { x // x ∈ s }, p.1 ∈ s,
(fun p : { x // x ∈ s } => ⟨p.val, h p⟩ : { x // x ∈ s } → { x // x ∈ s }) = id :=
fun _ => funext fun _ => Subtype.eq rfl
have :
∀ (t) (eq : s.ndinsert a = t),
t.attach = ndinsert ⟨a, eq ▸ mem_ndinsert_self a s⟩ (s.attach.map fun p => ⟨p.1, eq ▸ mem_ndinsert_of_mem p.2⟩) :=
by
intro t ht
by_cases h : a ∈ s
· rw [ndinsert_of_mem h] at ht
subst ht
rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]
· rw [ndinsert_of_notMem h] at ht
subst ht
simp [attach_cons, h]
this _ rfl
