exact Ultrafilter.union_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✝
ihp :
  ∀ {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} ∈ 𝓤
ihq :
  ∀ {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