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

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : maximalConsistentTheory consisT ⊢! p
⊢ p ∈ maximalConsistentTheory consisT
Tactic:
have : p ∈ theory (maximalConsistentTheory consisT) := h
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : maximalConsistentTheory consisT ⊢! p
this : p ∈ theory (maximalConsistentTheory consisT)
⊢ p ∈ maximalConsistentTheory consisT

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
p : Formula α
h : maximalConsistentTheory consisT ⊢! p
this : p ∈ theory (maximalConsistentTheory consisT)
⊢ p ∈ maximalConsistentTheory consisT
Tactic:
simpa using this
State after:
no goals