case a
α : Type u_1
β : Type ?u.394964
γ : Type ?u.394967
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)
α : Type u_1
β : Type ?u.394964
γ : Type ?u.394967
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s ∩ t) = min (count a s) (count a t)
apply @Nat.add_left_cancel (count a (s - t))
no goals
case a
α : Type u_1
β : Type ?u.394964
γ : Type ?u.394967
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)
rw [← count_add, sub_add_inter, count_sub, tsub_add_min]