Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_falsum (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:
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.1
⊢ False

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
⊢ False
Tactic:
have : 𝓓 ⊬! [⊥].conj' ⟶ [].disj' := t.consistent (by simpa) (by simp)
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
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.1
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.1
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.1
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.1
⊢ ∀ p ∈ [⊥], p ∈ t.tableau.1
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.1
⊢ ∀ p ∈ [], p ∈ t.tableau.2
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.1
this : 𝓓 ⊬! [⊥].conj' ⟶ [].disj'
⊢ 𝓓 ⊢! [⊥].conj' ⟶ [].disj'
Tactic:
simp
State after:
no goals