case hand =>
  exact Filter.inter_mem_iff.symm
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✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
a✝ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤 ∧
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝ ∧
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈
      𝓤
no goals