no goals
α : Type u_1
β : Type ?u.38177
γ : Type ?u.38180
ι : Sort ?u.38183
ι' : Sort ?u.38186
l l' : Filter α
p : ι → Prop
s : ι → Set α
t✝ : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
t U : Set α
⊢ U ∈ 𝓟 t ↔ ∃ i, True ∧ t ⊆ U
simp