[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
⊢ Set.univ ∈ {s | ∀ᶠ (a : α) in f, ∀ᶠ (b : β) in g, (a, b) ∈ s}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Set.mem_univ, eventually_true]
