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