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.1 ↔ p ∈ t.2
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.1 → p ∈ t.2

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.2 → p ∉ t.1

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.1 → p ∈ t.2

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.2 → p ∉ t.1
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.2 → p ∉ t.1

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.2 → p ∉ t.1
Tactic:
. apply Set.disjoint_right.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.1 → p ∈ t.2
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.2 → p ∉ t.1
Tactic:
apply Set.disjoint_right.mp $ disjoint_of_consistent hCon
State after:
no goals