if hyp : a = a0 then
  simp [mul_cons_trivial, mul_erase_trivial] at *
  aesop
else
  have a0_a: a0 ≠ a := by rw [eq_comm] at hyp; exact hyp
  ext b
  simp [Multiset.count_cons, Multiset.count_singleton, Multiset.count_add]
  have H : Multiset.count b (a ::ₘ M) = Multiset.count b (X + {a0}) := by aesop
  if ba : b = a then
    rw [ba]
    rw [ba] at H
    have : a ∈ X + {a0} := by
      by_contra h
      have absurd3 : Multiset.count a (a ::ₘ M) > 0 := by simp
      aesop
    have : Multiset.count a (a ::ₘ M) = Multiset.count a M + 1 := by simp
    have : Multiset.count a (a0 ::ₘ X) = Multiset.count a (Multiset.erase (a0 ::ₘ X) a) + 1 := by simp ; aesop
    aesop
  else 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}
⊢ M = X + {a0} - {a}
no goals