no goals
ι : Type u_2
α : ι → Type u_1
β : ι → Type ?u.156455
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ pi univ t₁ ⊆ pi univ t₂ ↔ (∀ (i : ι), t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅
simp [pi_subset_pi_iff]