no goals
α : Type u_1
β : Type ?u.189863
γ : Type ?u.189866
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a b : α
s t u : Multiset α
⊢ s + t ∩ u = (s + t) ∩ (s + u)
rw [add_comm, inter_add_distrib, add_comm s, add_comm s]