no goals
α : Type u_3
β : Type ?u.41707
γ : Type ?u.41710
ι✝ : Sort ?u.41713
ι'✝ : Sort ?u.41716
l✝ l' : Filter α
p✝ : ι✝ → Prop
s✝ : ι✝ → Set α
t✝ : Set α
i : ι✝
p' : ι'✝ → Prop
s' : ι'✝ → Set α
i' : ι'✝
ι : Sort u_1
ι' : ι → Type u_2
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), HasBasis (l i) (p i) (s i)
t : Set α
⊢ (t ∈ ⨆ (i : ι), l i) ↔ ∃ i, (∀ (i_1 : ι), p i_1 (i i_1)) ∧ (⋃ (i_1 : ι), s i_1 (i i_1)) ⊆ t
simp only [hasBasis_iff, (hl _).mem_iff, Classical.skolem, forall_and, iUnion_subset_iff,
  mem_iSup]