Theorem: LO.FirstOrder.Semiformula.val_Uprod (Logic/FirstOrder/Ultraproduct.lean)

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 : Formula L μ
⊢ (Evalfm (Uprod A 𝓤) ε) p ↔ {i | (Evalf (s i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
simp[Evalf, eval_Uprod, Matrix.empty_eq]
State after:
no goals