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

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
⊢ p ∈ maximalConsistentTheory consisT ∧ q ∈ maximalConsistentTheory consisT
Tactic:
have : maximalConsistentTheory consisT ⊢! p ⋏ q := mem_maximalConsistentTheory_iff.mp h
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ p ∈ maximalConsistentTheory consisT ∧ q ∈ maximalConsistentTheory consisT

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ p ∈ maximalConsistentTheory consisT ∧ q ∈ maximalConsistentTheory consisT
Tactic:
exact ⟨mem_maximalConsistentTheory_iff.mpr (by prover [this]),
       mem_maximalConsistentTheory_iff.mpr (by prover [this])⟩
State after:
no goals

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ maximalConsistentTheory consisT ⊢! p
Tactic:
prover [this]
State after:
no goals

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p q : Formula α
h : p ⋏ q ∈ maximalConsistentTheory consisT
this : maximalConsistentTheory consisT ⊢! p ⋏ q
⊢ maximalConsistentTheory consisT ⊢! q
Tactic:
prover [this]
State after:
no goals