internlm/Lean-Github huggingface dataset:
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
h : t₁.1 = t₂.1
⊢ t₁.2 = t₂.2
Tactic:
apply Set.eq_of_subset_of_subset
Proof state after:
case mp.a
α : 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

case mp.a
α : 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
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mp.a
α : 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

case mp.a
α : 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
Tactic:
. intro p hp;
  apply not_mem₁_iff_mem₂ ct₂ |>.mp; rw [←h];
  apply not_mem₁_iff_mem₂ ct₁ |>.mpr hp;
Proof state after:
case mp.a
α : 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
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mp.a
α : 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
Tactic:
. 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.a
α : 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
Tactic:
intro p hp
Proof state after:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₁.2
⊢ p ∈ t₂.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₁.2
⊢ p ∈ t₂.2
Tactic:
apply not_mem₁_iff_mem₂ ct₂ |>.mp
Proof state after:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₁.2
⊢ p ∉ t₂.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₁.2
⊢ p ∉ t₂.1
Tactic:
rw [←h]
Proof state after:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₁.2
⊢ p ∉ t₁.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₁.2
⊢ p ∉ t₁.1
Tactic:
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.a
α : 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
Tactic:
intro p hp
Proof state after:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₂.2
⊢ p ∈ t₁.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₂.2
⊢ p ∈ t₁.2
Tactic:
apply not_mem₁_iff_mem₂ ct₁ |>.mp
Proof state after:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₂.2
⊢ p ∉ t₁.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₂.2
⊢ p ∉ t₁.1
Tactic:
rw [h]
Proof state after:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₂.2
⊢ p ∉ t₂.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mp.a
α : 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
p : Formula α
hp : p ∈ t₂.2
⊢ p ∉ t₂.1
Tactic:
apply not_mem₁_iff_mem₂ ct₂ |>.mpr hp
Proof state after:
no goals
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
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
h : 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
h : t₁.2 = t₂.2
⊢ t₁.1 = t₂.1
Tactic:
apply Set.eq_of_subset_of_subset
Proof state after:
case mpr.a
α : 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₁.2 = t₂.2
⊢ t₁.1 ⊆ t₂.1

case mpr.a
α : 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₁.2 = t₂.2
⊢ t₂.1 ⊆ t₁.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mpr.a
α : 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₁.2 = t₂.2
⊢ t₁.1 ⊆ t₂.1

case mpr.a
α : 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₁.2 = t₂.2
⊢ t₂.1 ⊆ t₁.1
Tactic:
. 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.a
α : 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₁.2 = t₂.2
⊢ t₂.1 ⊆ t₁.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mpr.a
α : 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₁.2 = t₂.2
⊢ t₂.1 ⊆ t₁.1
Tactic:
. 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 mpr.a
α : 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₁.2 = t₂.2
⊢ t₁.1 ⊆ t₂.1
Tactic:
intro p hp
Proof state after:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₁.1
⊢ p ∈ t₂.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₁.1
⊢ p ∈ t₂.1
Tactic:
apply not_mem₂_iff_mem₁ ct₂ |>.mp
Proof state after:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₁.1
⊢ p ∉ t₂.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₁.1
⊢ p ∉ t₂.2
Tactic:
rw [←h]
Proof state after:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₁.1
⊢ p ∉ t₁.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₁.1
⊢ p ∉ t₁.2
Tactic:
apply not_mem₂_iff_mem₁ ct₁ |>.mpr hp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mpr.a
α : 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₁.2 = t₂.2
⊢ t₂.1 ⊆ t₁.1
Tactic:
intro p hp
Proof state after:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₂.1
⊢ p ∈ t₁.1
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₂.1
⊢ p ∈ t₁.1
Tactic:
apply not_mem₂_iff_mem₁ ct₁ |>.mp
Proof state after:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₂.1
⊢ p ∉ t₁.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₂.1
⊢ p ∉ t₁.2
Tactic:
rw [h]
Proof state after:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₂.1
⊢ p ∉ t₂.2
Theorem: LO.Propositional.Superintuitionistic.Tableau.saturated_duality
Proof state before:
case mpr.a
α : 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₁.2 = t₂.2
p : Formula α
hp : p ∈ t₂.1
⊢ p ∉ t₂.2
Tactic:
apply not_mem₂_iff_mem₁ ct₂ |>.mpr hp
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
⊢ (𝓓)-Consistent (Ax(𝓓), ∅)
Tactic:
intro Γ Δ hΓ hΔ
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : ∀ p ∈ Δ, p ∈ (Ax(𝓓), ∅).2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : ∀ p ∈ Δ, p ∈ (Ax(𝓓), ∅).2
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
replace hΔ : Δ = [] := List.nil_iff.mpr hΔ
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
obtain ⟨q, hq⟩ := h.exists_unprovable
Proof state after:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
by_contra hC
Proof state after:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False
Tactic:
have : 𝓓 ⊢! q := by
  subst hΔ;
  simp [List.disj'_nil] at hC;
  exact imp_trans! hC efq! ⨀ (by
    apply iff_provable_list_conj.mpr;
    exact λ _ hp => ⟨Deduction.eaxm $ hΓ _ hp⟩;
  );
Proof state after:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! q
⊢ False
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
case intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! q
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
hΔ : Δ = []
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ 𝓓 ⊢! q
Tactic:
subst hΔ
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ [].disj'
⊢ 𝓓 ⊢! q
Theorem: LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ [].disj'
⊢ 𝓓 ⊢! q
Tactic:
simp [List.disj'_nil] at hC
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ 𝓓 ⊢! q