exact Filter.univ_mem
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
e : Fin n✝ → Uprod A 𝓤
⊢ Set.univ ∈ 𝓤
no goals