Theorem: mem_erase_cons (Pdl/MultisetOrder.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a0 : α
M : Multiset α
x✝ : a0 ∈ M
⊢ M = M - {a0} + {a0}
Tactic:
simp_all [mul_cons_trivial, mul_erase_trivial, Multiset.cons_erase]
State after:
no goals