Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_verum (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
⊢ ⊤ ∈ t.tableau.1
Tactic:
apply t.not_mem₂_iff_mem₁.mp
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
⊢ ⊤ ∉ t.tableau.2

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
⊢ ⊤ ∉ t.tableau.2
Tactic:
by_contra hC
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
⊢ False

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
⊢ False
Tactic:
have : 𝓓 ⊬! [].conj' ⟶ [⊤].disj' := t.consistent (by simp) (by simpa)
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
⊢ False

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
⊢ False
Tactic:
have : 𝓓 ⊢! [].conj' ⟶ [⊤].disj' := by simp;
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this✝ : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
this : 𝓓 ⊢! [].conj' ⟶ [⊤].disj'
⊢ False

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this✝ : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
this : 𝓓 ⊢! [].conj' ⟶ [⊤].disj'
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
⊢ ∀ p ∈ [], p ∈ t.tableau.1
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
⊢ ∀ p ∈ [⊤], p ∈ t.tableau.2
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
⊢ 𝓓 ⊢! [].conj' ⟶ [⊤].disj'
Tactic:
simp
State after:
no goals