Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₂_of_lt (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n : ℕ
h : m ≤ n
⊢ t[m].2 ⊆ t[n].2
Tactic:
induction h with
| refl => simp;
| step h ih =>
  simp [lindenbaum_next_indexed, lindenbaum_next];
  split;
  . split <;> tauto;
  . tauto;
State after:
no goals

State before:
case refl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n : ℕ
⊢ t[m].2 ⊆ t[m].2
Tactic:
simp
State after:
no goals

State before:
case step
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
⊢ t[m].2 ⊆ t[m✝.succ].2
Tactic:
simp [lindenbaum_next_indexed, lindenbaum_next]
State after:
case step
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
⊢ t[m].2 ⊆
    (match decode m✝ with
      | some p =>
        if (𝓓)-Consistent (insert p t[m✝].1, t[m✝].2) then (insert p t[m✝].1, t[m✝].2) else (t[m✝].1, insert p t[m✝].2)
      | none => t[m✝]).2

State before:
case step
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
⊢ t[m].2 ⊆
    (match decode m✝ with
      | some p =>
        if (𝓓)-Consistent (insert p t[m✝].1, t[m✝].2) then (insert p t[m✝].1, t[m✝].2) else (t[m✝].1, insert p t[m✝].2)
      | none => t[m✝]).2
Tactic:
split
State after:
case step.h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode m✝ = some p✝
⊢ t[m].2 ⊆
    (if (𝓓)-Consistent (insert p✝ t[m✝].1, t[m✝].2) then (insert p✝ t[m✝].1, t[m✝].2)
      else (t[m✝].1, insert p✝ t[m✝].2)).2

case step.h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].2 ⊆ t[m✝].2

State before:
case step.h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode m✝ = some p✝
⊢ t[m].2 ⊆
    (if (𝓓)-Consistent (insert p✝ t[m✝].1, t[m✝].2) then (insert p✝ t[m✝].1, t[m✝].2)
      else (t[m✝].1, insert p✝ t[m✝].2)).2

case step.h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].2 ⊆ t[m✝].2
Tactic:
. split <;> tauto;
State after:
case step.h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].2 ⊆ t[m✝].2

State before:
case step.h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].2 ⊆ t[m✝].2
Tactic:
. tauto;
State after:
no goals

State before:
case step.h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode m✝ = some p✝
⊢ t[m].2 ⊆
    (if (𝓓)-Consistent (insert p✝ t[m✝].1, t[m✝].2) then (insert p✝ t[m✝].1, t[m✝].2)
      else (t[m✝].1, insert p✝ t[m✝].2)).2
Tactic:
split <;> tauto
State after:
no goals

State before:
case step.h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].2 ⊆ t[m✝].2
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].2 ⊆ t[m✝].2
Tactic:
tauto
State after:
no goals