ofModelsElementaryDiagram — Mathlib

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⟩
Похожие утверждения