Theorem: LO.Propositional.Classical.maximalConsistentTheory_consistent' (Logic/Propositional/Classical/Basic/Completeness.lean)

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
⊢ p ∈ maximalConsistentTheory consisT → ~p ∉ maximalConsistentTheory consisT
Tactic:
intro h hn
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
⊢ False

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
⊢ False
Tactic:
have : Inconsistent (maximalConsistentTheory consisT) :=
  System.inconsistent_iff_provable_bot.mpr
    (by prover [mem_maximalConsistentTheory_iff.mp h, mem_maximalConsistentTheory_iff.mp hn])
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
this : Inconsistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
have := this.not_con
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
this✝ : Inconsistent (maximalConsistentTheory consisT)
this : ¬Consistent (maximalConsistentTheory consisT)
⊢ False
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : p ∈ maximalConsistentTheory consisT
hn : ~p ∈ maximalConsistentTheory consisT
⊢ maximalConsistentTheory consisT ⊢! ⊥
Tactic:
prover [mem_maximalConsistentTheory_iff.mp h, mem_maximalConsistentTheory_iff.mp hn]
State after:
no goals