α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : Sentence L
⊢ Formula.Realize φ default ↔ ∀ᶠ (a : α) in ↑u, Formula.Realize φ default
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : Sentence L
⊢ Product (↑u) M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ
simp_rw [Sentence.Realize]
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : Sentence L
⊢ Formula.Realize φ default = Formula.Realize φ fun i => Quotient.mk' fun a => default i
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : Sentence L
⊢ Formula.Realize φ default ↔ ∀ᶠ (a : α) in ↑u, Formula.Realize φ default
erw [← realize_formula_cast φ, iff_eq_eq]
no goals
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → Structure L (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : Sentence L
⊢ Formula.Realize φ default = Formula.Realize φ fun i => Quotient.mk' fun a => default i
exact congr rfl (Subsingleton.elim _ _)