Lean4
/-- The canonical elementary embedding of an `L`-structure into any model of its elementary diagram
-/
@[simps]
def ofModelsElementaryDiagram (N : Type*) [L.Structure N] [L[[M]].Structure N] [(lhomWithConstants L M).IsExpansionOn N]
[N ⊨ L.elementaryDiagram M] : M ↪ₑ[L] N :=
⟨((↑) : L[[M]].Constants → N) ∘ Sum.inr, fun n φ x =>
by
refine
_root_.trans ?_
((realize_iff_of_model_completeTheory M N
(((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)).alls).trans
?_)
·
simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff, Function.comp_def, Term.realize_constants]
· simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff]
rfl⟩