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

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
i : ℕ
⊢ (𝓓)-Consistent t[i]
Tactic:
induction i with
| zero => simpa;
| succ i ih => apply lindenbaum_next_indexed_parametricConsistent_succ; assumption;
State after:
no goals

State before:
case zero
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
⊢ (𝓓)-Consistent t[0]
Tactic:
simpa
State after:
no goals

State before:
case succ
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
i : ℕ
ih : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i + 1]
Tactic:
apply lindenbaum_next_indexed_parametricConsistent_succ
State after:
case succ.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
i : ℕ
ih : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i]

State before:
case succ.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
consistent : (𝓓)-Consistent t
i : ℕ
ih : (𝓓)-Consistent t[i]
⊢ (𝓓)-Consistent t[i]
Tactic:
assumption
State after:
no goals