no goals
α : Type u_1
β : Type ?u.423349
γ : Type ?u.423352
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x : α
⊢ s ∩ replicate n x = replicate (min (count x s) n) x
rw [inter_comm, replicate_inter, min_comm]