internlm/Lean-Github huggingface dataset:
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
⊢ False
Tactic:
have thm₁ := BTheorem.transitivity prf₃.toTheorem (BTheorem.orI₁ : BTheorem (w₁ ⊃ w₁ ¦ w₂))
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
⊢ False
Tactic:
have thm₂ := BTheorem.transitivity prf₄.toTheorem (BTheorem.orI₂ : BTheorem (w₂ ⊃ w₁ ¦ w₂))
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
⊢ False
Tactic:
have thm₃ := BTheorem.mp (BTheorem.adj thm₂ thm₁) BTheorem.orE
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
⊢ False
Tactic:
have ⟨prf₅⟩ := h₄
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
h₄ :
  (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
    ▲lindenbaumSequence t Δ (i, j + 0)
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
w₂ : Form
prf₂ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) w₂
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₃ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁} w₁
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₄ : BProof {Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂} w₂
thm₁ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
thm₂ : BTheorem (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst lst₂⊃w₁¦w₂)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
⊢ False
Tactic:
clear h₄ thm₁ thm₂ prf₁ prf₂ prf₃ prf₄
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₁ : List Form
l₆ : { x | x ∈ lst₁ } ⊆ lindenbaumSequence t Δ (i, j + 0)
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd lst₁⊃w₁¦w₂)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
⊢ False
Tactic:
cases lst₁
Proof state after:
case nil
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
⊢ False

case cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head✝ : Form
tail✝ : List Form
l₆ : { x | x ∈ head✝ :: tail✝ } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
case cons.nil
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head✝ : Form
tail✝ : List Form
l₆ : { x | x ∈ head✝ :: tail✝ } ⊆ lindenbaumSequence t Δ (i, j + 0)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False

case cons.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head✝¹ : Form
tail✝¹ : List Form
l₆ : { x | x ∈ head✝¹ :: tail✝¹ } ⊆ lindenbaumSequence t Δ (i, j + 0)
head✝ : Form
tail✝ : List Form
l₇ : { x | x ∈ head✝ :: tail✝ } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head✝ :: tail✝)¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝¹ :: tail✝¹)⊃w₁¦w₂)
⊢ False
Tactic:
case' cons.nil head tail => 
  have := BProof.proveList l₆
  have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
  have := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
  have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
  exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
Proof state after:
case cons.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head✝¹ : Form
tail✝¹ : List Form
l₆ : { x | x ∈ head✝¹ :: tail✝¹ } ⊆ lindenbaumSequence t Δ (i, j + 0)
head✝ : Form
tail✝ : List Form
l₇ : { x | x ∈ head✝ :: tail✝ } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head✝ :: tail✝)¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝¹ :: tail✝¹)⊃w₁¦w₂)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
case cons.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head✝¹ : Form
tail✝¹ : List Form
l₆ : { x | x ∈ head✝¹ :: tail✝¹ } ⊆ lindenbaumSequence t Δ (i, j + 0)
head✝ : Form
tail✝ : List Form
l₇ : { x | x ∈ head✝ :: tail✝ } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head✝ :: tail✝)¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝¹ :: tail✝¹)⊃w₁¦w₂)
⊢ False
Tactic:
case' cons.cons head tail head' tail'=> 
  have prf₆ := BProof.proveList l₆
  have prf₇ := BProof.proveList l₇
  have := BProof.mp (BProof.adj prf₅ prf₇) BTheorem.distRight
  have prf₈ := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
  have := BProof.mp (BProof.adj prf₈ prf₆) BTheorem.distRight
  have prf₉ := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
  have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₉ thm₃⟩, l₅⟩
  exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
case cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
lst₂ : List Form
l₇ : { x | x ∈ lst₂ } ⊆ lindenbaumSequence t Δ (i, j + 0)
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head✝ : Form
tail✝ : List Form
l₆ : { x | x ∈ head✝ :: tail✝ } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          lst₂¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False
Tactic:
cases lst₂
Proof state after:
case cons.nil
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head✝ : Form
tail✝ : List Form
l₆ : { x | x ∈ head✝ :: tail✝ } ⊆ lindenbaumSequence t Δ (i, j + 0)
l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝ :: tail✝)⊃w₁¦w₂)
⊢ False

case cons.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head✝¹ : Form
tail✝¹ : List Form
l₆ : { x | x ∈ head✝¹ :: tail✝¹ } ⊆ lindenbaumSequence t Δ (i, j + 0)
head✝ : Form
tail✝ : List Form
l₇ : { x | x ∈ head✝ :: tail✝ } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head✝ :: tail✝)¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head✝¹ :: tail✝¹)⊃w₁¦w₂)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
case nil.nil
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
⊢ False
Tactic:
have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
Proof state after:
case nil.nil
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
case nil.nil
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ l₇ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          []¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False
Tactic:
exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
case nil.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
head : Form
tail : List Form
l₇ : { x | x ∈ head :: tail } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head :: tail)¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
⊢ False
Tactic:
have := BProof.proveList l₇
Proof state after:
case nil.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
head : Form
tail : List Form
l₇ : { x | x ∈ head :: tail } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head :: tail)¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
this : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
case nil.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
head : Form
tail : List Form
l₇ : { x | x ∈ head :: tail } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head :: tail)¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
this : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
⊢ False
Tactic:
have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
Proof state after:
case nil.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
l₆ : { x | x ∈ [] } ⊆ lindenbaumSequence t Δ (i, j + 0)
head : Form
tail : List Form
l₇ : { x | x ∈ head :: tail } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head :: tail)¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd []⊃w₁¦w₂)
this✝ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
this :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j +
              0)).fst&Form.conjoinList head
          tail)¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
⊢ False