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

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