L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable {φ, Formula.not φ}
⊢ False
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
⊢ False
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
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
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable {φ, Formula.not φ}
⊢ False
refine' h (p.isMaximal.1.mono _)
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
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
rw [insert_subset, singleton_subset_iff]
no goals
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
exact ⟨ht, hf⟩
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
L : Language
T : Theory L
α : Type w
p : CompleteType T α
φ : Sentence (L[[α]])
hf : Formula.not φ ∈ p
ht : φ ∈ p
⊢ ¬IsSatisfiable {φ, Formula.not φ}
rintro ⟨@⟨_, _, h, _⟩⟩
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
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
simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h
no goals
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
exact h.2 h.1