internlm/Lean-Github huggingface dataset:
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].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
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].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
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].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
Tactic:
. 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 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
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].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
⊢ i ≤ i + n
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].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
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].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
q : Formula α
hq : q ∈ Δ
⊢ q ∈ t[i + n].2
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].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
q : Formula α
hq : q ∈ Δ
⊢ q ∈ t[i + n].2
Tactic:
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:
α : 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
q : Formula α
hq : q ∈ Δ
⊢ n ≤ i + n
Tactic:
simp
Proof state after:
no goals
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'
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:
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 : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
⊢ ∀ p ∈ Γ, p ∈ t[n].1
Tactic:
intro p hp
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
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
p : Formula α
hp : p ∈ Γ
⊢ p ∈ t[n].1
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 : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hm : m < n
p : Formula α
hp : p ∈ Γ
⊢ p ∈ t[n].1
Tactic:
exact lindenbaum_next_indexed_subset₁_of_lt hm.le $ hΓ p hp
Proof state after:
no goals
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'
Tactic:
subst hmn
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
hΔ : ∀ p ∈ Δ, p ∈ t[m].2
⊢ 𝓓 ⊬! Γ.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
hΔ : ∀ p ∈ Δ, p ∈ t[m].2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
exact lindenbaum_next_indexed_parametricConsistent hCon m hΓ hΔ
Proof state after:
no goals
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 : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
⊢ ∀ p ∈ Δ, p ∈ t[m].2
Tactic:
intro p hp
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
m : ℕ
hΓ : ∀ p ∈ Γ, p ∈ t[m].1
n : ℕ
hΔ : ∀ p ∈ Δ, p ∈ t[n].2
hn : n < m
p : Formula α
hp : p ∈ Δ
⊢ p ∈ t[m].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
Γ Δ : 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
p : Formula α
hp : p ∈ Δ
⊢ p ∈ t[m].2
Tactic:
exact lindenbaum_next_indexed_subset₂_of_lt hn.le $ hΔ p hp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.lindenbaum
Proof 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
Proof 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
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.lindenbaum
Proof 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⟩
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.equality_of₁
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
⊢ t₁ = t₂
Tactic:
have e := Tableau.equality_def.mpr ⟨e₁, (saturated_duality.mp e₁)⟩
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ t₁ = t₂
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.equality_of₁
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ t₁ = t₂
Tactic:
calc
  t₁ = ⟨t₁.tableau, t₁.saturated, t₁.consistent⟩ := by rfl;
  _  = ⟨t₂.tableau, t₂.saturated, t₂.consistent⟩ := by simp [e];
  _  = t₂                                        := by rfl;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.equality_of₁
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ t₁ = { tableau := t₁.tableau, saturated := ⋯, consistent := ⋯ }
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.equality_of₁
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ { tableau := t₁.tableau, saturated := ⋯, consistent := ⋯ } =
    { tableau := t₂.tableau, saturated := ⋯, consistent := ⋯ }
Tactic:
simp [e]
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.equality_of₁
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
e₁ : t₁.tableau.1 = t₂.tableau.1
e : t₁.tableau = t₂.tableau
⊢ { tableau := t₂.tableau, saturated := ⋯, consistent := ⋯ } = t₂
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mdp₁
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
h : 𝓓 ⊢! p ⟶ q
⊢ q ∈ t.tableau.1
Tactic:
exact t.not_mem₂_iff_mem₁.mp $ not_mem₂ (by simpa) (show 𝓓 ⊢! List.conj' [p] ⟶ q by simpa;)
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mdp₁
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
h : 𝓓 ⊢! p ⟶ q
⊢ ∀ p_1 ∈ [p], p_1 ∈ t.tableau.1
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mdp₁
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
h : 𝓓 ⊢! p ⟶ q
⊢ 𝓓 ⊢! [p].conj' ⟶ q
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_verum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
⊢ ⊤ ∈ t.tableau.1
Tactic:
apply t.not_mem₂_iff_mem₁.mp
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
⊢ ⊤ ∉ t.tableau.2
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_verum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
⊢ ⊤ ∉ t.tableau.2
Tactic:
by_contra hC
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_verum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
⊢ False
Tactic:
have : 𝓓 ⊬! [].conj' ⟶ [⊤].disj' := t.consistent (by simp) (by simpa)
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_verum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
⊢ False
Tactic:
have : 𝓓 ⊢! [].conj' ⟶ [⊤].disj' := by simp;
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this✝ : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
this : 𝓓 ⊢! [].conj' ⟶ [⊤].disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_verum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this✝ : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
this : 𝓓 ⊢! [].conj' ⟶ [⊤].disj'
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_verum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
⊢ ∀ p ∈ [], p ∈ t.tableau.1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_verum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
⊢ ∀ p ∈ [⊤], p ∈ t.tableau.2
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_verum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊤ ∈ t.tableau.2
this : 𝓓 ⊬! [].conj' ⟶ [⊤].disj'
⊢ 𝓓 ⊢! [].conj' ⟶ [⊤].disj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_falsum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
⊢ ⊥ ∉ t.tableau.1
Tactic:
by_contra hC
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_falsum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
⊢ False
Tactic:
have : 𝓓 ⊬! [⊥].conj' ⟶ [].disj' := t.consistent (by simpa) (by simp)
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
this : 𝓓 ⊬! [⊥].conj' ⟶ [].disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_falsum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
this : 𝓓 ⊬! [⊥].conj' ⟶ [].disj'
⊢ False
Tactic:
have : 𝓓 ⊢! [⊥].conj' ⟶ [].disj' := by simp;
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
this✝ : 𝓓 ⊬! [⊥].conj' ⟶ [].disj'
this : 𝓓 ⊢! [⊥].conj' ⟶ [].disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_falsum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
this✝ : 𝓓 ⊬! [⊥].conj' ⟶ [].disj'
this : 𝓓 ⊢! [⊥].conj' ⟶ [].disj'
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_falsum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
⊢ ∀ p ∈ [⊥], p ∈ t.tableau.1
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_falsum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
⊢ ∀ p ∈ [], p ∈ t.tableau.2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_falsum
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
hC : ⊥ ∈ t.tableau.1
this : 𝓓 ⊬! [⊥].conj' ⟶ [].disj'
⊢ 𝓓 ⊢! [⊥].conj' ⟶ [].disj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋏ q ∈ t.tableau.1 ↔ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋏ q ∈ t.tableau.1 → p ∈ t.tableau.1 ∧ q ∈ t.tableau.1

case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1 → p ⋏ q ∈ t.tableau.1