internlm/Lean-Github huggingface dataset:
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
⊢ (𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2)
Tactic:
by_contra hC
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬((𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2))
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬((𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2))
⊢ False
Tactic:
push_neg at hC
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
⊢ False
Tactic:
have ⟨hC₁, hC₂⟩ := hC
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
⊢ False
Tactic:
obtain ⟨Γ₁, Δ₁, hΓ₁, hΔ₁, h₁⟩ := iff_not_ParametricConsistent_insert₁.mp hC₁
Proof state after:
case intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! p ⋏ Γ₁.conj' ⟶ Δ₁.disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
case intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! p ⋏ Γ₁.conj' ⟶ Δ₁.disj'
⊢ False
Tactic:
replace h₁ := imply_left_and_comm'! h₁
Proof state after:
case intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
case intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
⊢ False
Tactic:
obtain ⟨Γ₂, Δ₂, hΓ₂, hΔ₂, h₂⟩ := iff_not_ParametricConsistent_insert₂.mp hC₂
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
⊢ False
Tactic:
have : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj' := imp_trans! (conj₁'! iff_concat_conj!) $ imp_trans! (cut! h₁ h₂) (conj₂'! iff_concact_disj!)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ False
Tactic:
have : 𝓓 ⊬! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj' := hCon (by simp; rintro q (hq₁ | hq₂); exact hΓ₁ q hq₁; exact hΓ₂ q hq₂) (by simp; rintro q (hq₁ | hq₂); exact hΔ₁ q hq₁; exact hΔ₂ q hq₂)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this✝ : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
this : 𝓓 ⊬! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this✝ : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
this : 𝓓 ⊬! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ p ∈ Γ₁ ++ Γ₂, p ∈ t.1
Tactic:
simp
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ (p : Formula α), p ∈ Γ₁ ∨ p ∈ Γ₂ → p ∈ t.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ (p : Formula α), p ∈ Γ₁ ∨ p ∈ Γ₂ → p ∈ t.1
Tactic:
rintro q (hq₁ | hq₂)
Proof state after:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₁ : q ∈ Γ₁
⊢ q ∈ t.1

case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Γ₂
⊢ q ∈ t.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₁ : q ∈ Γ₁
⊢ q ∈ t.1

case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Γ₂
⊢ q ∈ t.1
Tactic:
exact hΓ₁ q hq₁
Proof state after:
case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Γ₂
⊢ q ∈ t.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Γ₂
⊢ q ∈ t.1
Tactic:
exact hΓ₂ q hq₂
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ p ∈ Δ₁ ++ Δ₂, p ∈ t.2
Tactic:
simp
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ (p : Formula α), p ∈ Δ₁ ∨ p ∈ Δ₂ → p ∈ t.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ (p : Formula α), p ∈ Δ₁ ∨ p ∈ Δ₂ → p ∈ t.2
Tactic:
rintro q (hq₁ | hq₂)
Proof state after:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₁ : q ∈ Δ₁
⊢ q ∈ t.2

case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Δ₂
⊢ q ∈ t.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₁ : q ∈ Δ₁
⊢ q ∈ t.2

case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Δ₂
⊢ q ∈ t.2
Tactic:
exact hΔ₁ q hq₁
Proof state after:
case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Δ₂
⊢ q ∈ t.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either
Proof state before:
case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Δ₂
⊢ q ∈ t.2
Tactic:
exact hΔ₂ q hq₂
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.disjoint_of_consistent
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
⊢ Disjoint t.1 t.2
Tactic:
by_contra h
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.disjoint_of_consistent
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
⊢ False
Tactic:
obtain ⟨T, hp₁, hp₂, hp⟩ := by simpa [Disjoint] using h;
Proof state after:
case intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp : ¬T ⊆ ∅
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.disjoint_of_consistent
Proof state before:
case intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp : ¬T ⊆ ∅
⊢ False
Tactic:
obtain ⟨p, hp, _⟩ := Set.not_subset.mp hp
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.disjoint_of_consistent
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
⊢ False
Tactic:
simp [ParametricConsistent] at hCon
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
⊢ False