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

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i + 1]
Tactic:
simp [lindenbaum_next_indexed]
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
⊢ (𝓓)-Consistent t[i] →
    (𝓓)-Consistent
      (match decode i with
      | some p => lindenbaum_next 𝓓 p t[i]
      | none => t[i])

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
⊢ (𝓓)-Consistent t[i] →
    (𝓓)-Consistent
      (match decode i with
      | some p => lindenbaum_next 𝓓 p t[i]
      | none => t[i])
Tactic:
split
State after:
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])

case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]

State before:
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])

case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]
Tactic:
. intro h; apply next_parametericConsistent; assumption;
State after:
case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]

State before:
case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]
Tactic:
. tauto;
State after:
no goals

State before:
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])
Tactic:
intro h
State after:
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
h : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])

State before:
case h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
h : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent (lindenbaum_next 𝓓 p✝ t[i])
Tactic:
apply next_parametericConsistent
State after:
case h_1.consistent
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
h : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i]

State before:
case h_1.consistent
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode i = some p✝
h : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i]
Tactic:
assumption
State after:
no goals

State before:
case h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
i : ℕ
x✝ : Option (Formula α)
heq✝ : decode i = none
⊢ (𝓓)-Consistent t[i] → (𝓓)-Consistent t[i]
Tactic:
tauto
State after:
no goals