if ba0 : b = a0 then
rw [ba0]
rw [ba0] at H
have : Multiset.count a0 (Multiset.erase (a ::ₘ M) a) = Multiset.count a0 (Multiset.erase (a ::ₘ M) a) := by
simp
have : Multiset.count a0 (a ::ₘ M) = Multiset.count a0 X + 1 := by subst_eqs; rw [mul_cons_trivial] at H; simp_all
have : Multiset.count a0 M = Multiset.count a0 (a ::ₘ M) := by
have : a0 ≠ a := by simp_all
rw [Multiset.count_cons_of_ne this M]
simp_all
else
have : Multiset.count b M = Multiset.count b (a ::ₘ M) := by
have : b ≠ a := by simp_all
rw [Multiset.count_cons_of_ne this M]
rw [this ]
have : Multiset.count b (X + {a0}) = Multiset.count b (Multiset.erase (a0 ::ₘ X) a) := by
simp
simp_all
simp_all
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H✝ : a ::ₘ M = X + {a0}
hyp : ¬a = a0
a0_a : a0 ≠ a
b : α
H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0})
ba : ¬b = a
⊢ Multiset.count b M = (Multiset.count b X + if b = a0 then 1 else 0) - if b = a then 1 else 0
no goals