-- Mathlib/ModelTheory/Types.lean
theorem not_mem_iff (p : T.CompleteType α) (φ : L[[α]].Sentence) : φ.not ∈ p ↔ ¬φ ∈ p :=
  ⟨fun hf ht => by
    have h : ¬IsSatisfiable ({φ, φ.not} : L[[α]].Theory)

Proof state:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬{φ, Formula.not φ}.IsSatisfiable
⊢ False

Tactic:
refine h (p.isMaximal.1.mono ?_)

Result:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬{φ, Formula.not φ}.IsSatisfiable
⊢ {φ, Formula.not φ} ⊆ ↑p

Proof state:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
⊢ ¬{φ, Formula.not φ}.IsSatisfiable

Tactic:
rintro ⟨@⟨_, _, h, _⟩⟩

Result:
case intro.mk
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier✝ : Type (max (max u w) v)
struc✝ : L[[α]].Structure Carrier✝
h : Carrier✝ ⊨ {φ, Formula.not φ}
nonempty'✝ : Nonempty Carrier✝
⊢ False

Proof state:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬{φ, Formula.not φ}.IsSatisfiable
⊢ {φ, Formula.not φ} ⊆ ↑p

Tactic:
rw [insert_subset_iff, singleton_subset_iff]

Result:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬{φ, Formula.not φ}.IsSatisfiable
⊢ φ ∈ ↑p ∧ Formula.not φ ∈ ↑p

Proof state:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
⊢ False

Tactic:
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

Result:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬{φ, Formula.not φ}.IsSatisfiable
⊢ False

Proof state:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬{φ, Formula.not φ}.IsSatisfiable
⊢ φ ∈ ↑p ∧ Formula.not φ ∈ ↑p

Tactic:
exact ⟨ht, hf⟩

Result:
no goals

Proof state:
case intro.mk
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier✝ : Type (max (max u w) v)
struc✝ : L[[α]].Structure Carrier✝
h : Carrier✝ ⊨ {φ, Formula.not φ}
nonempty'✝ : Nonempty Carrier✝
⊢ False

Tactic:
simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h

Result:
case intro.mk
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier✝ : Type (max (max u w) v)
struc✝ : L[[α]].Structure Carrier✝
nonempty'✝ : Nonempty Carrier✝
h : Carrier✝ ⊨ φ ∧ Carrier✝ ⊨ Formula.not φ
⊢ False

Proof state:
case intro.mk
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier✝ : Type (max (max u w) v)
struc✝ : L[[α]].Structure Carrier✝
nonempty'✝ : Nonempty Carrier✝
h : Carrier✝ ⊨ φ ∧ Carrier✝ ⊨ Formula.not φ
⊢ False

Tactic:
exact h.2 h.1

Result:
no goals