Theorem: LO.FirstOrder.models_Uprod (Logic/FirstOrder/Ultraproduct.lean)

State before:
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
inst✝¹ : Nonempty I
inst✝ : ∀ (i : I), Nonempty (A i)
σ : Sentence L
⊢ Uprod A 𝓤 ⊧ₘ σ ↔ {i | A i ⊧ₘ σ} ∈ 𝓤
Tactic:
simp[models_def, Semiformula.val_Uprod, Empty.eq_elim]
State after:
no goals