internlm/Lean-Github huggingface dataset:
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 : ∀ {Γ Δ : 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
Tactic:
have : 𝓓 ⊬! [p].conj' ⟶ [p].disj' := hCon
  (by simp_all; apply hp₁; assumption)
  (by simp_all; apply hp₂; assumption)
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 ∉ ∅
this : 𝓓 ⊬! [p].conj' ⟶ [p].disj'
⊢ 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 : ∀ {Γ Δ : 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 ∉ ∅
this : 𝓓 ⊬! [p].conj' ⟶ [p].disj'
⊢ False
Tactic:
have : 𝓓 ⊢! [p].conj' ⟶ [p].disj' := by simp;
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 ∉ ∅
this✝ : 𝓓 ⊬! [p].conj' ⟶ [p].disj'
this : 𝓓 ⊢! [p].conj' ⟶ [p].disj'
⊢ 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 : ∀ {Γ Δ : 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 ∉ ∅
this✝ : 𝓓 ⊬! [p].conj' ⟶ [p].disj'
this : 𝓓 ⊢! [p].conj' ⟶ [p].disj'
⊢ False
Tactic:
contradiction
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
h : ¬Disjoint t.1 t.2
⊢ ?m.113495
Tactic:
simpa [Disjoint] using h
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 : ∀ {Γ Δ : 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 ∉ ∅
⊢ ∀ p_1 ∈ [p], p_1 ∈ t.1
Tactic:
simp_all
Proof state after:
α : 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
⊢ p ∈ t.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.disjoint_of_consistent
Proof state before:
α : 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
⊢ p ∈ t.1
Tactic:
apply hp₁
Proof state after:
case a
α : 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
⊢ p ∈ T
Theorem: LO.Propositional.Superintuitionistic.Tableau.disjoint_of_consistent
Proof state before:
case a
α : 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
⊢ p ∈ T
Tactic:
assumption
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 : ∀ {Γ Δ : 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 ∉ ∅
⊢ ∀ p_1 ∈ [p], p_1 ∈ t.2
Tactic:
simp_all
Proof state after:
α : 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
⊢ p ∈ t.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.disjoint_of_consistent
Proof state before:
α : 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
⊢ p ∈ t.2
Tactic:
apply hp₂
Proof state after:
case a
α : 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
⊢ p ∈ T
Theorem: LO.Propositional.Superintuitionistic.Tableau.disjoint_of_consistent
Proof state before:
α : 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 ∉ ∅
this : 𝓓 ⊬! [p].conj' ⟶ [p].disj'
⊢ 𝓓 ⊢! [p].conj' ⟶ [p].disj'
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
⊢ q ∉ t.2
Tactic:
by_contra hC
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
⊢ False
Tactic:
have : 𝓓 ⊢! Γ.conj' ⟶ [q].disj' := by simpa;
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
⊢ False
Tactic:
have : 𝓓 ⊬! Γ.conj' ⟶ [q].disj' := hCon (by aesop) (by aesop)
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this✝ : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
this : 𝓓 ⊬! Γ.conj' ⟶ [q].disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this✝ : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
this : 𝓓 ⊬! Γ.conj' ⟶ [q].disj'
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
⊢ 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
⊢ ∀ p ∈ Γ, p ∈ t.1
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
q : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ t.1
h : 𝓓 ⊢! Γ.conj' ⟶ q
hC : q ∈ t.2
this : 𝓓 ⊢! Γ.conj' ⟶ [q].disj'
⊢ ∀ p ∈ [q], p ∈ t.2
Tactic:
aesop
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem₂_of_not_mem₁
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.1 → p ∈ t.2
Tactic:
intro h
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.1
⊢ p ∈ t.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem₂_of_not_mem₁
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.1
⊢ p ∈ t.2
Tactic:
cases (hMat p) with
| inl h' => exact absurd h' h;
| inr _ => assumption;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem₂_of_not_mem₁
Proof state before:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.1
h' : p ∈ t.1
⊢ p ∈ t.2
Tactic:
exact absurd h' h
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem₂_of_not_mem₁
Proof state before:
case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.1
h✝ : p ∈ t.2
⊢ p ∈ t.2
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem₁_of_not_mem₂
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.2 → p ∈ t.1
Tactic:
intro h
Proof state after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.2
⊢ p ∈ t.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem₁_of_not_mem₂
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.2
⊢ p ∈ t.1
Tactic:
cases (hMat p) with
| inl _ => assumption;
| inr h' => exact absurd h' h;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem₁_of_not_mem₂
Proof state before:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.2
h✝ : p ∈ t.1
⊢ p ∈ t.1
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.mem₁_of_not_mem₂
Proof state before:
case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
h : p ∉ t.2
h' : p ∈ t.2
⊢ p ∈ t.1
Tactic:
exact absurd h' h
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₁_iff_mem₂
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.1 ↔ p ∈ t.2
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.1 → p ∈ t.2

case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.2 → p ∉ t.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₁_iff_mem₂
Proof state before:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.1 → p ∈ t.2

case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.2 → p ∉ t.1
Tactic:
. apply mem₂_of_not_mem₁ hMat;
Proof state after:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.2 → p ∉ t.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₁_iff_mem₂
Proof state before:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.2 → p ∉ t.1
Tactic:
. apply Set.disjoint_right.mp $ disjoint_of_consistent hCon;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₁_iff_mem₂
Proof state before:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.1 → p ∈ t.2
Tactic:
apply mem₂_of_not_mem₁ hMat
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₁_iff_mem₂
Proof state before:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.2 → p ∉ t.1
Tactic:
apply Set.disjoint_right.mp $ disjoint_of_consistent hCon
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂_iff_mem₁
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.2 ↔ p ∈ t.1
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.2 → p ∈ t.1

case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.1 → p ∉ t.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂_iff_mem₁
Proof state before:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.2 → p ∈ t.1

case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.1 → p ∉ t.2
Tactic:
. apply mem₁_of_not_mem₂ hMat;
Proof state after:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.1 → p ∉ t.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂_iff_mem₁
Proof state before:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.1 → p ∉ t.2
Tactic:
. apply Set.disjoint_left.mp $ disjoint_of_consistent hCon;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂_iff_mem₁
Proof state before:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∉ t.2 → p ∈ t.1
Tactic:
apply mem₁_of_not_mem₂ hMat
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.not_mem₂_iff_mem₁
Proof state before:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
p : Formula α
⊢ p ∈ t.1 → p ∉ t.2
Tactic:
apply Set.disjoint_left.mp $ disjoint_of_consistent hCon
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
⊢ t₁.1 = t₂.1 ↔ t₁.2 = t₂.2
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
⊢ t₁.1 = t₂.1 → t₁.2 = t₂.2

case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
⊢ t₁.2 = t₂.2 → t₁.1 = t₂.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
⊢ t₁.1 = t₂.1 → t₁.2 = t₂.2

case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
⊢ t₁.2 = t₂.2 → t₁.1 = t₂.1
Tactic:
. intro h;
  apply Set.eq_of_subset_of_subset;
  . intro p hp;
    apply not_mem₁_iff_mem₂ ct₂ |>.mp; rw [←h];
    apply not_mem₁_iff_mem₂ ct₁ |>.mpr hp;
  . intro p hp;
    apply not_mem₁_iff_mem₂ ct₁ |>.mp; rw [h];
    apply not_mem₁_iff_mem₂ ct₂ |>.mpr hp;
Proof state after:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
⊢ t₁.2 = t₂.2 → t₁.1 = t₂.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mpr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
⊢ t₁.2 = t₂.2 → t₁.1 = t₂.1
Tactic:
. intro h;
  apply Set.eq_of_subset_of_subset;
  . intro p hp;
    apply not_mem₂_iff_mem₁ ct₂ |>.mp; rw [←h];
    apply not_mem₂_iff_mem₁ ct₁ |>.mpr hp;
  . intro p hp;
    apply not_mem₂_iff_mem₁ ct₁ |>.mp; rw [h];
    apply not_mem₂_iff_mem₁ ct₂ |>.mpr hp;
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
⊢ t₁.1 = t₂.1 → t₁.2 = t₂.2
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
h : t₁.1 = t₂.1
⊢ t₁.2 = t₂.2