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