Theorem: LO.Propositional.Superintuitionistic.Tableau.mem₂_of_not_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:
intro h
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.1
⊢ p ∈ t.2

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 α
h : p ∉ t.1
⊢ p ∈ t.2
Tactic:
cases (hMat p) with
| inl h' => exact absurd h' h;
| inr _ => assumption;
State after:
no goals

State before:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.1
h' : p ∈ t.1
⊢ p ∈ t.2
Tactic:
exact absurd h' h
State after:
no goals

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