[GOAL]
L : Language
T : Theory L
α : Type w
p q : CompleteType T α
h : (fun p => ↑p) p = (fun p => ↑p) q
⊢ p = q
[PROOFSTEP]
cases p
[GOAL]
case mk
L : Language
T : Theory L
α : Type w
q : CompleteType T α
toTheory✝ : Theory (L[[α]])
subset'✝ : LHom.onTheory (lhomWithConstants L α) T ⊆ toTheory✝
isMaximal'✝ : IsMaximal toTheory✝
h : (fun p => ↑p) { toTheory := toTheory✝, subset' := subset'✝, isMaximal' := isMaximal'✝ } = (fun p => ↑p) q
⊢ { toTheory := toTheory✝, subset' := subset'✝, isMaximal' := isMaximal'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
L : Language
T : Theory L
α : Type w
toTheory✝¹ : Theory (L[[α]])
subset'✝¹ : LHom.onTheory (lhomWithConstants L α) T ⊆ toTheory✝¹
isMaximal'✝¹ : IsMaximal toTheory✝¹
toTheory✝ : Theory (L[[α]])
subset'✝ : LHom.onTheory (lhomWithConstants L α) T ⊆ toTheory✝
isMaximal'✝ : IsMaximal toTheory✝
h :
  (fun p => ↑p) { toTheory := toTheory✝¹, subset' := subset'✝¹, isMaximal' := isMaximal'✝¹ } =
    (fun p => ↑p) { toTheory := toTheory✝, subset' := subset'✝, isMaximal' := isMaximal'✝ }
⊢ { toTheory := toTheory✝¹, subset' := subset'✝¹, isMaximal' := isMaximal'✝¹ } =
    { toTheory := toTheory✝, subset' := subset'✝, isMaximal' := isMaximal'✝ }
[PROOFSTEP]
congr
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
⊢ False
[PROOFSTEP]
have h : ¬IsSatisfiable ({ φ, φ.not } : L[[α]].Theory) :=
  by
  rintro ⟨@⟨_, _, h, _⟩⟩
  simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h 
  exact h.2 h.1
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
⊢ ¬IsSatisfiable {φ, Formula.not φ}
[PROOFSTEP]
rintro ⟨@⟨_, _, h, _⟩⟩
[GOAL]
case intro.mk
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier✝ : Type (max (max u w) v)
struc✝ : Structure (L[[α]]) Carrier✝
h : Carrier✝ ⊨ {φ, Formula.not φ}
nonempty'✝ : Nonempty Carrier✝
⊢ False
[PROOFSTEP]
simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h 
[GOAL]
case intro.mk
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier✝ : Type (max (max u w) v)
struc✝ : Structure (L[[α]]) Carrier✝
nonempty'✝ : Nonempty Carrier✝
h : Carrier✝ ⊨ φ ∧ Carrier✝ ⊨ Formula.not φ
⊢ False
[PROOFSTEP]
exact h.2 h.1
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable {φ, Formula.not φ}
⊢ False
[PROOFSTEP]
refine' h (p.isMaximal.1.mono _)
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable {φ, Formula.not φ}
⊢ {φ, Formula.not φ} ⊆ ↑p
[PROOFSTEP]
rw [insert_subset_iff, singleton_subset_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable {φ, Formula.not φ}
⊢ φ ∈ ↑p ∧ Formula.not φ ∈ ↑p
[PROOFSTEP]
exact ⟨ht, hf⟩
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ {p | S ⊆ ↑p} = ∅ ↔ ¬IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
[PROOFSTEP]
rw [iff_not_comm, ← not_nonempty_iff_eq_empty, Classical.not_not, Set.Nonempty]
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S) ↔ ∃ x, x ∈ {p | S ⊆ ↑p}
[PROOFSTEP]
refine'
  ⟨fun h =>
    ⟨⟨L[[α]].completeTheory h.some, (subset_union_left _ S).trans completeTheory.subset,
        completeTheory.isMaximal (L[[α]]) h.some⟩,
      (subset_union_right ((L.lhomWithConstants α).onTheory T) _).trans completeTheory.subset⟩,
    _⟩
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ (∃ x, x ∈ {p | S ⊆ ↑p}) → IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
[PROOFSTEP]
rintro ⟨p, hp⟩
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
p : CompleteType T α
hp : p ∈ {p | S ⊆ ↑p}
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ S)
[PROOFSTEP]
exact p.isMaximal.1.mono (union_subset p.subset hp)
[GOAL]
L : Language
T : Theory L
α : Type w
φ : Sentence (L[[α]])
⊢ {p | φ ∈ p} = Set.univ ↔ LHom.onTheory (lhomWithConstants L α) T ⊨ᵇ φ
[PROOFSTEP]
rw [models_iff_not_satisfiable, ← compl_empty_iff, compl_setOf_mem, ← setOf_subset_eq_empty_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
φ : Sentence (L[[α]])
⊢ {p | Formula.not φ ∈ p} = ∅ ↔ {p | {Formula.not φ} ⊆ ↑p} = ∅
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ (φ : Sentence (L[[α]])), φ ∈ S → LHom.onTheory (lhomWithConstants L α) T ⊨ᵇ φ
[PROOFSTEP]
have h : {p : T.CompleteType α | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S) :=
  by
  ext
  simp [subset_def]
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
x✝ : CompleteType T α
⊢ x✝ ∈ {p | S ⊆ ↑p} ↔ x✝ ∈ ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
[PROOFSTEP]
simp [subset_def]
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ (φ : Sentence (L[[α]])), φ ∈ S → LHom.onTheory (lhomWithConstants L α) T ⊨ᵇ φ
[PROOFSTEP]
simp_rw [h, sInter_eq_univ, ← setOf_mem_eq_univ_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ (s : Set (CompleteType T α)), s ∈ (fun φ => {p | φ ∈ p}) '' S → s = Set.univ) ↔
    ∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ
[PROOFSTEP]
refine' ⟨fun h φ φS => h _ ⟨_, φS, rfl⟩, _⟩
[GOAL]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ) →
    ∀ (s : Set (CompleteType T α)), s ∈ (fun φ => {p | φ ∈ p}) '' S → s = Set.univ
[PROOFSTEP]
rintro h _ ⟨φ, h1, rfl⟩
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h✝ : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
h : ∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ
φ : Sentence (L[[α]])
h1 : φ ∈ S
⊢ (fun φ => {p | φ ∈ p}) φ = Set.univ
[PROOFSTEP]
exact h _ h1
[GOAL]
L : Language
T : Theory L
α : Type w
⊢ Nonempty (CompleteType T α) ↔ IsSatisfiable T
[PROOFSTEP]
rw [← isSatisfiable_onTheory_iff (lhomWithConstants_injective L α)]
[GOAL]
L : Language
T : Theory L
α : Type w
⊢ Nonempty (CompleteType T α) ↔ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T)
[PROOFSTEP]
rw [nonempty_iff_univ_nonempty, nonempty_iff_ne_empty, Ne.def, not_iff_comm, ←
  union_empty ((L.lhomWithConstants α).onTheory T), ← setOf_subset_eq_empty_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
⊢ {p | ∅ ⊆ ↑p} = ∅ ↔ Set.univ = ∅
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
ι : Type u_1
S : ι → Theory (L[[α]])
⊢ ⋂ (i : ι), {p | S i ⊆ ↑p} = {p | ⋃ (i : ι), S i ⊆ ↑p}
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
T : Theory L
α : Type w
ι : Type u_1
S : ι → Theory (L[[α]])
x✝ : CompleteType T α
⊢ x✝ ∈ ⋂ (i : ι), {p | S i ⊆ ↑p} ↔ x✝ ∈ {p | ⋃ (i : ι), S i ⊆ ↑p}
[PROOFSTEP]
simp only [mem_iInter, mem_setOf_eq, iUnion_subset_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
t : Finset (Sentence (L[[α]]))
⊢ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (Finset.toList t) ∈ p ↔ ↑t ⊆ ↑p
[PROOFSTEP]
simp_rw [subset_def, ← SetLike.mem_coe, p.isMaximal.mem_iff_models, models_sentence_iff, Sentence.Realize,
  Formula.Realize, BoundedFormula.realize_foldr_inf, Finset.mem_toList]
[GOAL]
L : Language
T : Theory L
α : Type w
p : CompleteType T α
t : Finset (Sentence (L[[α]]))
⊢ (∀ (M : ModelType ↑p) (φ : BoundedFormula (L[[α]]) Empty 0), φ ∈ t → BoundedFormula.Realize φ default default) ↔
    ∀ (x : Sentence (L[[α]])), x ∈ ↑t → ∀ (M : ModelType ↑p), BoundedFormula.Realize x default default
[PROOFSTEP]
exact ⟨fun h φ hφ M => h _ _ hφ, fun h M φ hφ => h _ hφ _⟩
[GOAL]
L : Language
T : Theory L
α : Type w
M : Type w'
inst✝² : Structure L M
inst✝¹ : Nonempty M
inst✝ : M ⊨ T
v : α → M
φ : Formula L α
⊢ ↑Formula.equivSentence φ ∈ typeOf T v ↔ Formula.Realize φ v
[PROOFSTEP]
simp
[GOAL]
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) α
[PROOFSTEP]
obtain ⟨M⟩ := p.isMaximal.1
[GOAL]
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) α
[PROOFSTEP]
refine' ⟨(M.subtheoryModel p.subset).reduct (L.lhomWithConstants α), fun a => (L.con a : M), _⟩
[GOAL]
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
[PROOFSTEP]
refine' SetLike.ext fun φ => _
[GOAL]
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
[PROOFSTEP]
simp only [CompleteType.mem_typeOf]
[GOAL]
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
[PROOFSTEP]
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)
[GOAL]
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 ⊨ φ
[PROOFSTEP]
rfl
