no goals
ι : Type u_1
α : ι → Type u_2
β : Type ?u.1273
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
⊢ Finset.Nonempty (Finset.sigma s t) ↔ ∃ i, i ∈ s ∧ Finset.Nonempty (t i)
simp [Finset.Nonempty]