internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case intro.intro.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hmn : m = n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
. exact lindenbaum_next_indexed_parametricConsistent hCon n (by intro p hp; exact lindenbaum_next_indexed_subset₁_of_lt hm.le $ hΓ p hp) hΔ;
Proof state after:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hmn : m = n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case intro.intro.inr.inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hmn : m = n
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
. subst hmn;
  exact lindenbaum_next_indexed_parametricConsistent hCon m hΓ hΔ;
Proof state after:
case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case intro.intro.inr.inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
. exact lindenbaum_next_indexed_parametricConsistent hCon m hΓ (by intro p hp; exact lindenbaum_next_indexed_subset₂_of_lt hn.le $ hΔ p hp);
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
⊢ ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
Tactic:
induction Γ with
| nil => simp;
| cons p Γ ih =>
  simp_all;
  obtain ⟨i, hi⟩ := hΓ.1;
  obtain ⟨m, hm⟩ := ih;
  use (i + m);
  constructor;
  . exact lindenbaum_next_indexed_subset₁_of_lt (by simp) hi;
  . intro q hq;
    exact lindenbaum_next_indexed_subset₁_of_lt (by simp) $ hm q hq;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case nil
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
hΓ : ∀ p ∈ [], ∃ i, p ∈ t[i].1
⊢ ∃ m, ∀ p ∈ [], p ∈ t[m].1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
ih : (∀ p ∈ Γ, ∃ i, p ∈ t[i].1) → ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : ∀ p_1 ∈ p :: Γ, ∃ i, p_1 ∈ t[i].1
⊢ ∃ m, ∀ p_1 ∈ p :: Γ, p_1 ∈ t[m].1
Tactic:
simp_all
Proof state after:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
ih : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
ih : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1
Tactic:
obtain ⟨i, hi⟩ := hΓ.1
Proof state after:
case cons.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
ih : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case cons.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
ih : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1
Tactic:
obtain ⟨m, hm⟩ := ih
Proof state after:
case cons.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case cons.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∃ m, p ∈ t[m].1 ∧ ∀ a ∈ Γ, a ∈ t[m].1
Tactic:
use (i + m)
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ p ∈ t[i + m].1 ∧ ∀ a ∈ Γ, a ∈ t[i + m].1
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ p ∈ t[i + m].1 ∧ ∀ a ∈ Γ, a ∈ t[i + m].1
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ p ∈ t[i + m].1

case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∀ a ∈ Γ, a ∈ t[i + m].1
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ p ∈ t[i + m].1

case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∀ a ∈ Γ, a ∈ t[i + m].1
Tactic:
. exact lindenbaum_next_indexed_subset₁_of_lt (by simp) hi;
Proof state after:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∀ a ∈ Γ, a ∈ t[i + m].1
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∀ a ∈ Γ, a ∈ t[i + m].1
Tactic:
. intro q hq;
  exact lindenbaum_next_indexed_subset₁_of_lt (by simp) $ hm q hq;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ p ∈ t[i + m].1
Tactic:
exact lindenbaum_next_indexed_subset₁_of_lt (by simp) hi
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ i ≤ i + m
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∀ a ∈ Γ, a ∈ t[i + m].1
Tactic:
intro q hq
Proof state after:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
q : Formula α
hq : q ∈ Γ
⊢ q ∈ t[i + m].1
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
q : Formula α
hq : q ∈ Γ
⊢ q ∈ t[i + m].1
Tactic:
exact lindenbaum_next_indexed_subset₁_of_lt (by simp) $ hm q hq
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
p : Formula α
Γ : List (Formula α)
hΓ : (∃ i, p ∈ t[i].1) ∧ ∀ a ∈ Γ, ∃ i, a ∈ t[i].1
i : ℕ
hi : p ∈ t[i].1
m : ℕ
hm : ∀ p ∈ Γ, p ∈ t[m].1
q : Formula α
hq : q ∈ Γ
⊢ m ≤ i + m
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
⊢ ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
Tactic:
induction Δ with
| nil => simp;
| cons p Δ ih =>
  simp_all;
  obtain ⟨i, hi⟩ := hΔ.1;
  obtain ⟨n, hn⟩ := ih;
  use (i + n);
  constructor;
  . exact lindenbaum_next_indexed_subset₂_of_lt (by simp) hi;
  . intro q hq;
    exact lindenbaum_next_indexed_subset₂_of_lt (by simp) $ hn q hq;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case nil
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
hΔ : ∀ p ∈ [], ∃ i, p ∈ t[i].2
⊢ ∃ n, ∀ p ∈ [], p ∈ t[n].2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : (∀ p ∈ Δ, ∃ i, p ∈ t[i].2) → ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : ∀ p_1 ∈ p :: Δ, ∃ i, p_1 ∈ t[i].2
⊢ ∃ n, ∀ p_1 ∈ p :: Δ, p_1 ∈ t[n].2
Tactic:
simp_all
Proof state after:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case cons
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2
Tactic:
obtain ⟨i, hi⟩ := hΔ.1
Proof state after:
case cons.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case cons.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
ih : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2
Tactic:
obtain ⟨n, hn⟩ := ih
Proof state after:
case cons.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case cons.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ ∃ n, p ∈ t[n].2 ∧ ∀ a ∈ Δ, a ∈ t[n].2
Tactic:
use (i + n)
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ p ∈ t[i + n].2 ∧ ∀ a ∈ Δ, a ∈ t[i + n].2
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ p ∈ t[i + n].2 ∧ ∀ a ∈ Δ, a ∈ t[i + n].2
Tactic:
constructor
Proof state after:
case h.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ p ∈ t[i + n].2

case h.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ : List (Formula α)
hΓ✝ : ∀ p ∈ Γ, ∃ i, p ∈ t[i].1
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
p : Formula α
Δ : List (Formula α)
hΔ : (∃ i, p ∈ t[i].2) ∧ ∀ a ∈ Δ, ∃ i, a ∈ t[i].2
i : ℕ
hi : p ∈ t[i].2
n : ℕ
hn : ∀ p ∈ Δ, p ∈ t[n].2
⊢ ∀ a ∈ Δ, a ∈ t[i + n].2