internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₁_of_lt
Proof 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].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode m✝ = some p✝
⊢ t[m].1 ⊆
    (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)).1

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].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].1 ⊆ t[m✝].1
Tactic:
. split <;> tauto;
Proof 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].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].1 ⊆ t[m✝].1
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₁_of_lt
Proof 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].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].1 ⊆ t[m✝].1
Tactic:
. tauto;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₁_of_lt
Proof 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].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode m✝ = some p✝
⊢ t[m].1 ⊆
    (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)).1
Tactic:
split <;> tauto
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₁_of_lt
Proof 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].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].1 ⊆ t[m✝].1
Tactic:
tauto
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₂_of_lt
Proof 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;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₂_of_lt
Proof 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
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₂_of_lt
Proof 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]
Proof 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
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₂_of_lt
Proof 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
Proof 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
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₂_of_lt
Proof 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;
Proof 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
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₂_of_lt
Proof 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;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₂_of_lt
Proof 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
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₂_of_lt
Proof 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
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
⊢ ∃ u, t ⊆ u ∧ (𝓓)-Consistent u ∧ u.Saturated
Tactic:
use t∞
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t ⊆ t∞ ∧ (𝓓)-Consistent t∞ ∧ t∞.Saturated
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
⊢ t ⊆ t∞ ∧ (𝓓)-Consistent t∞ ∧ t∞.Saturated
Tactic:
refine ⟨?subset, ?consistent, ?saturated⟩
Proof state after:
case subset
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t ⊆ t∞

case consistent
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ (𝓓)-Consistent t∞

case saturated
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
⊢ t∞.Saturated
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
⊢ t ⊆ t∞
Tactic:
case subset => constructor <;> apply Set.subset_iUnion_of_subset 0 (by 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
⊢ t∞.Saturated
Tactic:
case saturated =>
  intro p;
  cases mem_lindenbaum_next_indexed t p with
  | inl h => left; simp [lindenbaum_maximal]; use (encode p + 1);
  | inr h => right; simp [lindenbaum_maximal]; use (encode p + 1);
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
⊢ (𝓓)-Consistent t∞
Tactic:
case consistent =>
  intro Γ Δ hΓ hΔ;
  simp_all [lindenbaum_maximal];
  obtain ⟨m, hΓ⟩ : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1 := by
    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;
  obtain ⟨n, hΔ⟩ : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2 := by
    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;
  rcases (lt_trichotomy m n) with hm | hmn | hn;
  . exact lindenbaum_next_indexed_parametricConsistent hCon n (by intro p hp; exact lindenbaum_next_indexed_subset₁_of_lt hm.le $ hΓ p hp) hΔ;
  . subst hmn;
    exact lindenbaum_next_indexed_parametricConsistent hCon m hΓ hΔ;
  . 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
⊢ t ⊆ t∞
Tactic:
constructor <;> apply Set.subset_iUnion_of_subset 0 (by 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
⊢ t.2 ⊆ t[0].2
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
⊢ t∞.Saturated
Tactic:
intro p
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
⊢ p ∈ t∞.1 ∨ p ∈ t∞.2
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
p : Formula α
⊢ p ∈ t∞.1 ∨ p ∈ t∞.2
Tactic:
cases mem_lindenbaum_next_indexed t p with
| inl h => left; simp [lindenbaum_maximal]; use (encode p + 1);
| inr h => right; simp [lindenbaum_maximal]; use (encode p + 1);
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case inl
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ p ∈ t∞.1 ∨ p ∈ t∞.2
Tactic:
left
Proof state after:
case inl.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ p ∈ t∞.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case inl.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ p ∈ t∞.1
Tactic:
simp [lindenbaum_maximal]
Proof state after:
case inl.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ ∃ i, p ∈ t[i].1
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case inl.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ (lindenbaum_next_indexed ?m.372754 t (encode p + 1)).1
⊢ ∃ i, p ∈ t[i].1
Tactic:
use (encode p + 1)
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case inr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ t[encode p + 1].2
⊢ p ∈ t∞.1 ∨ p ∈ t∞.2
Tactic:
right
Proof state after:
case inr.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ t[encode p + 1].2
⊢ p ∈ t∞.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case inr.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ t[encode p + 1].2
⊢ p ∈ t∞.2
Tactic:
simp [lindenbaum_maximal]
Proof state after:
case inr.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ t[encode p + 1].2
⊢ ∃ i, p ∈ t[i].2
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case inr.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
p : Formula α
h : p ∈ t[encode p + 1].2
⊢ ∃ i, p ∈ t[i].2
Tactic:
use (encode p + 1)
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
⊢ (𝓓)-Consistent t∞
Tactic:
intro Γ Δ hΓ hΔ
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
hCon : (𝓓)-Consistent t
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t∞.1
hΔ : ∀ p ∈ Δ, p ∈ t∞.2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
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 ∈ Γ, p ∈ t∞.1
hΔ : ∀ p ∈ Δ, p ∈ t∞.2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
simp_all [lindenbaum_maximal]
Proof state after:
α : 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
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
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
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
obtain ⟨m, hΓ⟩ : ∃ m, ∀ p ∈ Γ, p ∈ t[m].1 := by
  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:
case 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
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case 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
hΔ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
obtain ⟨n, hΔ⟩ : ∃ n, ∀ p ∈ Δ, p ∈ t[n].2 := by
  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:
case 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
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau
Proof state before:
case 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
hΔ✝ : ∀ p ∈ Δ, ∃ i, p ∈ t[i].2
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
rcases (lt_trichotomy m n) with hm | hmn | hn
Proof state after:
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'