have := H0 b
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : b = a
⊢ Multiset.count a X = Multiset.count a (M - {a0}) + if a = a then 1 else 0
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : b = a
this : (Multiset.count b M + if b = a then 1 else 0) = Multiset.count b X + if b = a0 then 1 else 0
⊢ Multiset.count a X = Multiset.count a (M - {a0}) + if a = a then 1 else 0