Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.lindenbaum (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t₀ : Tableau α
hCon : (𝓓)-Consistent t₀
⊢ ∃ t, t₀ ⊆ t.tableau
Tactic:
obtain ⟨t, ht, hCon, hMax⟩ := Tableau.lindenbaum hCon
State after:
case intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t₀ : Tableau α
hCon✝ : (𝓓)-Consistent t₀
t : Tableau α
ht : t₀ ⊆ t
hCon : (𝓓)-Consistent t
hMax : t.Saturated
⊢ ∃ t, t₀ ⊆ t.tableau

State before:
case intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t₀ : Tableau α
hCon✝ : (𝓓)-Consistent t₀
t : Tableau α
ht : t₀ ⊆ t
hCon : (𝓓)-Consistent t
hMax : t.Saturated
⊢ ∃ t, t₀ ⊆ t.tableau
Tactic:
exact ⟨⟨t, hMax, hCon⟩, ht⟩
State after:
no goals