Theorem: mul_erase_trivial (Pdl/MultisetOrder.lean)

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

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ (M - {a}) = Multiset.count a✝ (M.erase a)
Tactic:
simp [Multiset.erase_singleton]
State after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ M - Multiset.count a✝ {a} = Multiset.count a✝ (M.erase a)

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ Multiset.count a✝ M - Multiset.count a✝ {a} = Multiset.count a✝ (M.erase a)
Tactic:
simp [Multiset.count_cons, Multiset.count_singleton, Multiset.count_add]
State after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ (Multiset.count a✝ M - if a✝ = a then 1 else 0) = Multiset.count a✝ (M.erase a)

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M : Multiset α
a✝ : α
⊢ (Multiset.count a✝ M - if a✝ = a then 1 else 0) = Multiset.count a✝ (M.erase a)
Tactic:
aesop
State after:
no goals