Theorem: neq_erase (Pdl/MultisetOrder.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M : Multiset α
x✝ : a0 ≠ a
⊢ Multiset.count a0 (M.erase a) = Multiset.count a0 M
Tactic:
have : Multiset.count a0 (a ::ₘ (Multiset.erase M a)) = Multiset.count a0 (a ::ₘ M) := by simp_all
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M : Multiset α
x✝ : a0 ≠ a
this : Multiset.count a0 (a ::ₘ M.erase a) = Multiset.count a0 (a ::ₘ M)
⊢ Multiset.count a0 (M.erase a) = Multiset.count a0 M

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M : Multiset α
x✝ : a0 ≠ a
this : Multiset.count a0 (a ::ₘ M.erase a) = Multiset.count a0 (a ::ₘ M)
⊢ Multiset.count a0 (M.erase a) = Multiset.count a0 M
Tactic:
simp_all
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M : Multiset α
x✝ : a0 ≠ a
⊢ Multiset.count a0 (a ::ₘ M.erase a) = Multiset.count a0 (a ::ₘ M)
Tactic:
simp_all
State after:
no goals