Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂ (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
⊢ q ∉ t.2
Tactic:
by_contra hC
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
⊢ False

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
⊢ False
Tactic:
have : 𝓓 ⊢! Γ.conj' ⟶ [q].disj' := by simpa;
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
⊢ False

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
⊢ False
Tactic:
have : 𝓓 ⊬! Γ.conj' ⟶ [q].disj' := hCon (by aesop) (by aesop)
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this✝ : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
this : 𝓓 ⊬! Γ.conj' ⟶ [q].disj'
⊢ False

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this✝ : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
this : 𝓓 ⊬! Γ.conj' ⟶ [q].disj'
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
⊢ 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
⊢ ∀ p ∈ Γ, p ∈ t.1
Tactic:
aesop
State after:
no goals

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
⊢ ∀ p ∈ [q], p ∈ t.2
Tactic:
aesop
State after:
no goals