English
If m is a multiset of cardinality n+1 and a ∈ m, then erasing a from the canonical Sym element mk m hc yields the canonical Sym element mk (m.erase a) with the appropriate card equality.
Русский
Пусть m — мультсет с кардинальностью n+1 и a ∈ m. Удаление a из символьного элемента mk m hc даёт элемент mk (m.erase a) с корректным равенством кардинальности.
LaTeX
$$$ (\mathrm{mk}\ m\ hc).\erase\ a\ h = \mathrm{mk}(m.erase a) \ (\text{card}(m.erase a) = n). $$$
Lean4
@[simp]
theorem erase_mk [DecidableEq α] (m : Multiset α) (hc : Multiset.card m = n + 1) (a : α) (h : a ∈ m) :
(mk m hc).erase a h = mk (m.erase a) (by rw [Multiset.card_erase_of_mem h, hc, Nat.add_one, Nat.pred_succ]) :=
rfl
