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