no goals
α : Type u_1
β : Type ?u.162424
γ : Type ?u.162427
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a b : α
s t : Multiset α
h : t ≤ s
⊢ ↑card s = ↑card t + ↑card (s - t)
rw [add_comm, ← card_add, tsub_add_cancel_of_le h]