Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
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
e : Fin n → Uprod A 𝓤
ε : μ → Uprod A 𝓤
p : Semiformula L μ n
⊢ (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
induction p using rec' <;>
simp[*, Prop.top_eq_true, Prop.bot_eq_false, eval_rel, eval_nrel, Semiterm.val_Uprod]
Proof state after:
case hverum
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 ∈ 𝓤

case hnrel
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✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ n✝
e : Fin n✝ → Uprod A 𝓤
⊢ {i | Structure.rel r✝ fun x => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v✝ x)} ∉ 𝓤 ↔
    {i | ¬Structure.rel r✝ fun i_1 => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v✝ i_1)} ∈ 𝓤

case hand
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✝} ∈
      𝓤

case hor
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✝} ∈
      𝓤

case hall
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✝ : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p✝} ∈ 𝓤) ↔
    {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤

case hex
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✝ : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∃ x, {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p✝} ∈ 𝓤) ↔
    {i | ∃ x, (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤