no goals
ι : Type ?u.895297
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
a : Multiset α
l : List (Multiset α)
⊢ Disjoint a (List.sum l) ↔ ∀ (b : Multiset α), b ∈ l → Disjoint a b
simpa only [@disjoint_comm _ a] using disjoint_list_sum_left