no goals
α : Type u_1
β : Type ?u.504974
γ : Type ?u.504977
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t = s ∪ t ↔ Disjoint s t
simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
  Nat.min_eq_zero_iff, Nat.add_eq_max_iff]