no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.289749
ι : Sort x
f : Filter (α → β)
g : Filter α
s : Set β
⊢ s ∈ seq f g ↔ ∃ u, u ∈ f ∧ ∃ t, t ∈ g ∧ Set.seq u t ⊆ s
simp only [mem_seq_def, seq_subset, exists_prop, iff_self_iff]