no goals
ι : Type u_1
α : ι → Type u_2
β : Type ?u.6768
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
⊢ Finset.sigma s t = ∅ ↔ ∀ (i : ι), i ∈ s → t i = ∅
simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists, not_and]