case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
⊢ ∃ M, p ∈ realizedTypes T (↑M) α
L : Language
T : Theory L
α : Type w
M : Type w'
inst✝² : Structure L M
inst✝¹ : Nonempty M
inst✝ : M ⊨ T
p : CompleteType T α
⊢ ∃ M, p ∈ realizedTypes T (↑M) α
obtain ⟨M⟩ := p.isMaximal.1
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
⊢ (typeOf T fun a => ↑(Language.con L a)) = p
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
⊢ ∃ M, p ∈ realizedTypes T (↑M) α
refine' ⟨(M.subtheoryModel p.subset).reduct (L.lhomWithConstants α), fun a => (L.con a : M), _⟩
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
φ : Sentence (L[[α]])
⊢ (φ ∈ typeOf T fun a => ↑(Language.con L a)) ↔ φ ∈ p
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
⊢ (typeOf T fun a => ↑(Language.con L a)) = p
refine' SetLike.ext fun φ => _
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
φ : Sentence (L[[α]])
⊢ (Formula.Realize (↑Formula.equivSentence.symm φ) fun a => ↑(Language.con L a)) ↔ φ ∈ p
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
φ : Sentence (L[[α]])
⊢ (φ ∈ typeOf T fun a => ↑(Language.con L a)) ↔ φ ∈ p
simp only [CompleteType.mem_typeOf]
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
φ : Sentence (L[[α]])
⊢ ↑(ModelType.reduct (lhomWithConstants L α)
          (ModelType.subtheoryModel M (_ : LHom.onTheory (lhomWithConstants L α) T ⊆ ↑p))) ⊨
      φ ↔
    ↑M ⊨ φ
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
φ : Sentence (L[[α]])
⊢ (Formula.Realize (↑Formula.equivSentence.symm φ) fun a => ↑(Language.con L a)) ↔ φ ∈ p
refine'
  (@Formula.realize_equivSentence_symm_con _
    ((M.subtheoryModel p.subset).reduct (L.lhomWithConstants α)) _ _ M.struc _ φ).trans
    (_root_.trans (_root_.trans _ (p.isMaximal.isComplete.realize_sentence_iff φ M))
      (p.isMaximal.mem_iff_models φ).symm)
no goals
case intro
L : Language
T : Theory L
α : Type w
M✝ : Type w'
inst✝² : Structure L M✝
inst✝¹ : Nonempty M✝
inst✝ : M✝ ⊨ T
p : CompleteType T α
M : ModelType ↑p
φ : Sentence (L[[α]])
⊢ ↑(ModelType.reduct (lhomWithConstants L α)
          (ModelType.subtheoryModel M (_ : LHom.onTheory (lhomWithConstants L α) T ⊆ ↑p))) ⊨
      φ ↔
    ↑M ⊨ φ
rfl