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

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.2 ↔ p ∈ t.1
Tactic:
constructor
State after:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.2 → p ∈ t.1

case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.1 → p ∉ t.2

State before:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.2 → p ∈ t.1

case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.1 → p ∉ t.2
Tactic:
. apply mem₁_of_not_mem₂ hMat;
State after:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.1 → p ∉ t.2

State before:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.1 → p ∉ t.2
Tactic:
. apply Set.disjoint_left.mp $ disjoint_of_consistent hCon;
State after:
no goals

State before:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.2 → p ∈ t.1
Tactic:
apply mem₁_of_not_mem₂ hMat
State after:
no goals

State before:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.1 → p ∉ t.2
Tactic:
apply Set.disjoint_left.mp $ disjoint_of_consistent hCon
State after:
no goals