no goals
ι : Type u_1
ι' : Type ?u.30556
α : ι → Type u_2
β : ι → Type ?u.30566
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
⊢ (¬∃ i, i ∈ s ∧ Set.Nonempty (t i)) ↔ ∀ (i : ι), i ∈ s → t i = ∅
simp only [not_nonempty_iff_eq_empty, not_and, not_exists]