case h.e'_2.a
ι : Type ?u.896168
β✝ : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β✝
β : Type u_1
i : Finset β
f : β → Multiset α
a : Multiset α
⊢ (∀ (b : β), b ∈ i → Disjoint (f b) a) ↔ ∀ (b : Multiset α), b ∈ map f i.val → Disjoint b a
ι : Type ?u.896168
β✝ : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β✝
β : Type u_1
i : Finset β
f : β → Multiset α
a : Multiset α
⊢ Disjoint (Finset.sum i f) a ↔ ∀ (b : β), b ∈ i → Disjoint (f b) a
convert @disjoint_sum_left _ a (map f i.val)
no goals
case h.e'_2.a
ι : Type ?u.896168
β✝ : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β✝
β : Type u_1
i : Finset β
f : β → Multiset α
a : Multiset α
⊢ (∀ (b : β), b ∈ i → Disjoint (f b) a) ↔ ∀ (b : Multiset α), b ∈ map f i.val → Disjoint b a
simp [and_congr_left_iff, iff_self_iff]