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

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
⊢ p ∈ t[encode p + 1].1 ∨ p ∈ t[encode p + 1].2
Tactic:
simp [lindenbaum_next_indexed, lindenbaum_next]
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
⊢ p ∈
      (if (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2) then (insert p t[encode p].1, t[encode p].2)
        else (t[encode p].1, insert p t[encode p].2)).1 ∨
    p ∈
      (if (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2) then (insert p t[encode p].1, t[encode p].2)
        else (t[encode p].1, insert p t[encode p].2)).2

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
⊢ p ∈
      (if (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2) then (insert p t[encode p].1, t[encode p].2)
        else (t[encode p].1, insert p t[encode p].2)).1 ∨
    p ∈
      (if (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2) then (insert p t[encode p].1, t[encode p].2)
        else (t[encode p].1, insert p t[encode p].2)).2
Tactic:
split
State after:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1 ∨ p ∈ (insert p t[encode p].1, t[encode p].2).2

case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).1 ∨ p ∈ (t[encode p].1, insert p t[encode p].2).2

State before:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1 ∨ p ∈ (insert p t[encode p].1, t[encode p].2).2

case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).1 ∨ p ∈ (t[encode p].1, insert p t[encode p].2).2
Tactic:
. left; tauto;
State after:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).1 ∨ p ∈ (t[encode p].1, insert p t[encode p].2).2

State before:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).1 ∨ p ∈ (t[encode p].1, insert p t[encode p].2).2
Tactic:
. right; tauto;
State after:
no goals

State before:
case isTrue
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1 ∨ p ∈ (insert p t[encode p].1, t[encode p].2).2
Tactic:
left
State after:
case isTrue.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1

State before:
case isTrue.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : (𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (insert p t[encode p].1, t[encode p].2).1
Tactic:
tauto
State after:
no goals

State before:
case isFalse
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).1 ∨ p ∈ (t[encode p].1, insert p t[encode p].2).2
Tactic:
right
State after:
case isFalse.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).2

State before:
case isFalse.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t✝ t : Tableau α
p : Formula α
h✝ : ¬(𝓓)-Consistent (insert p t[encode p].1, t[encode p].2)
⊢ p ∈ (t[encode p].1, insert p t[encode p].2).2
Tactic:
tauto
State after:
no goals