Theorem: mul_cons_trivial (Pdl/MultisetOrder.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
⊢ M + {a} = a ::ₘ M
Tactic:
ext
State after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ (M + {a}) = Multiset.count a✝ (a ::ₘ M)

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ (M + {a}) = Multiset.count a✝ (a ::ₘ M)
Tactic:
simp [Multiset.count_cons, Multiset.count_singleton, Multiset.count_add]
State after:
no goals