internlm/Lean-Github huggingface dataset:
Theorem: lindenbaumIsPrime
Proof state before:
case inl
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
⊢ (f ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev) ∨
    g ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev
Tactic:
apply Or.inl
Proof state after:
case inl.h
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
⊢ f ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev
Theorem: lindenbaumIsPrime
Proof state before:
case inr
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ¬▲(prev ∪ {f}) ∩ Δ = ∅
⊢ (f ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev) ∨
    g ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev
Tactic:
apply Or.inr
Proof state after:
case inr.h
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ¬▲(prev ∪ {f}) ∩ Δ = ∅
⊢ g ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev
Theorem: lindenbaumIsPrime
Proof state before:
case inl
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
⊢ f ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev
Tactic:
split
Proof state after:
case inl.inl
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
h✝ : f¦g ∈ ▲prev
⊢ f ∈ prev ∪ {f}

case inl.inr
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
h✝ : ¬f¦g ∈ ▲prev
⊢ f ∈ prev
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
h✝ : f¦g ∈ ▲prev
⊢ f ∈ prev ∪ {f}
Tactic:
case inl => exact Or.inr rfl
Proof state after:
no goals
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
h₂ : ¬f¦g ∈ ▲prev
⊢ f ∈ prev
Tactic:
case inr h₂ => exact False.elim $ h₂ ⟨BProof.ax l₂⟩
Proof state after:
no goals
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
h✝ : f¦g ∈ ▲prev
⊢ f ∈ prev ∪ {f}
Tactic:
exact Or.inr rfl
Proof state after:
no goals
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
prev : Ctx := lindenbaumSequence t Δ (i + 1, k)
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
h₁ : ▲(prev ∪ {f}) ∩ Δ = ∅
h₂ : ¬f¦g ∈ ▲prev
⊢ f ∈ prev
Tactic:
exact False.elim $ h₂ ⟨BProof.ax l₂⟩
Proof state after:
no goals
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
l₃ : f ∈ lindenbaumSequence t Δ (i + 1, k + 1) ∨ g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
⊢ f ∈ lindenbaumSequence t Δ (i + 1, k + 1) → f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
intros h₁
Proof state after:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
l₃ : f ∈ lindenbaumSequence t Δ (i + 1, k + 1) ∨ g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
h₁ : f ∈ lindenbaumSequence t Δ (i + 1, k + 1)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
l₃ : f ∈ lindenbaumSequence t Δ (i + 1, k + 1) ∨ g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
h₁ : f ∈ lindenbaumSequence t Δ (i + 1, k + 1)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
exact Or.inl ⟨⟨i+1,k+1⟩,h₁⟩
Proof state after:
no goals
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
l₃ : f ∈ lindenbaumSequence t Δ (i + 1, k + 1) ∨ g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
⊢ g ∈ lindenbaumSequence t Δ (i + 1, k + 1) → f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
intros h₁
Proof state after:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
l₃ : f ∈ lindenbaumSequence t Δ (i + 1, k + 1) ∨ g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
h₁ : g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
l₃ : f ∈ lindenbaumSequence t Δ (i + 1, k + 1) ∨ g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
h₁ : g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
exact Or.inr ⟨⟨i+1,k+1⟩,h₁⟩
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅
Tactic:
have l₁ := formalFixed t.property
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
l₁ : ▲↑t = ↑t
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
l₁ : ▲↑t = ↑t
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅
Tactic:
rw [←l₁] at h₁
Proof state after:
t : Th
Δ : Ctx
h₁ : ▲↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
l₁ : ▲↑t = ↑t
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ▲↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
l₁ : ▲↑t = ↑t
⊢ ▲lindenbaumSequence t Δ (0, 0) ∩ Δ = ∅
Tactic:
exact h₁
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ▲lindenbaumSequence t Δ (i + 1, 0) ∩ Δ = ∅
Tactic:
change
  ▲{ f : Form | ∃j : Nat, f ∈ lindenbaumSequence t Δ ⟨i, j⟩ } ∩ Δ = ∅
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ = ∅
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ = ∅
Tactic:
apply Set.not_nonempty_iff_eq_empty.mp
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ¬Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
⊢ ¬Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
Tactic:
intros h₃
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
h₃ : Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
h₃ : Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
⊢ False
Tactic:
have ⟨w,⟨prf₁⟩,l₁⟩ := h₃
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
h₃ : Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
h₃ : Set.Nonempty (▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } ∩ Δ)
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
⊢ False
Tactic:
clear h₃
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
⊢ False
Tactic:
have ⟨s,l₂,prf₂⟩ := BProof.compactness prf₁
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
⊢ False
Tactic:
have ⟨j, l₃⟩ := finiteExhaustion lindenbaumStageMonotone l₂
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
⊢ False
Tactic:
have l₄ := lindenbaumAvoids h₁ h₂ ⟨i,j⟩
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Tactic:
have prf₃ := BProof.monotone l₃ prf₂
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
prf₃ : BProof (lindenbaumSequence t Δ (i, j)) w
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
prf₃ : BProof (lindenbaumSequence t Δ (i, j)) w
⊢ False
Tactic:
have l₅ := Set.not_nonempty_iff_eq_empty.mpr l₄
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
prf₃ : BProof (lindenbaumSequence t Δ (i, j)) w
l₅ : ¬Set.Nonempty (▲lindenbaumSequence t Δ (i, j) ∩ Δ)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i : ℕ
w : Form
prf₁ : BProof { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) } w
l₁ : w ∈ Δ
s : Finset Form
l₂ : ↑s ⊆ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
prf₂ : BProof (↑s) w
j : ℕ
l₃ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₄ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
prf₃ : BProof (lindenbaumSequence t Δ (i, j)) w
l₅ : ¬Set.Nonempty (▲lindenbaumSequence t Δ (i, j) ∩ Δ)
⊢ False
Tactic:
exact l₅ ⟨w, ⟨⟨prf₃⟩,l₁⟩⟩
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
⊢ ▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ = ∅
Tactic:
apply Set.not_nonempty_iff_eq_empty.mp
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
⊢ ¬Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
⊢ ¬Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
Tactic:
intros h₃
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
⊢ False
Tactic:
have ⟨w₁,l₁,l₂⟩ := h₃
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₁ : w₁ ∈ ▲lindenbaumSequence t Δ (i, j + 1)
l₂ : w₁ ∈ Δ
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₁ : w₁ ∈ ▲lindenbaumSequence t Δ (i, j + 1)
l₂ : w₁ ∈ Δ
⊢ False
Tactic:
unfold lindenbaumSequence at l₁
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲match (i, j + 1) with
      | (0, 0) => ↑t
      | (Nat.succ i, 0) => { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
      | (i, Nat.succ j) =>
        let prev := lindenbaumSequence t Δ (i, j);
        let l := (Denumerable.ofNat (Form × Form) j).fst;
        let r := (Denumerable.ofNat (Form × Form) j).snd;
        if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲match (i, j + 1) with
      | (0, 0) => ↑t
      | (Nat.succ i, 0) => { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
      | (i, Nat.succ j) =>
        let prev := lindenbaumSequence t Δ (i, j);
        let l := (Denumerable.ofNat (Form × Form) j).fst;
        let r := (Denumerable.ofNat (Form × Form) j).snd;
        if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False
Tactic:
split at l₁
Proof state after:
case h_1
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
heq✝ : (i, j + 1) = (0, 0)
l₁ : w₁ ∈ ▲↑t
⊢ False

case h_2
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
i✝ : ℕ
heq✝ : (i, j + 1) = (Nat.succ i✝, 0)
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (i✝, j) }
⊢ False

case h_3
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
i✝ j✝ : ℕ
heq✝ : (i, j + 1) = (i✝, Nat.succ j✝)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i✝, j✝);
      let l := (Denumerable.ofNat (Form × Form) j✝).fst;
      let r := (Denumerable.ofNat (Form × Form) j✝).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
heq : (i, j + 1) = (0, 0)
l₁ : w₁ ∈ ▲↑t
⊢ False
Tactic:
case h_1 x heq => injection heq with heq; contradiction
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
x : ℕ
heq : (i, j + 1) = (Nat.succ x, 0)
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (x, j) }
⊢ False
Tactic:
case h_2 x heq => injection heq with heq; contradiction
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
heq : (i, j + 1) = (0, 0)
l₁ : w₁ ∈ ▲↑t
⊢ False
Tactic:
injection heq with heq
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
l₁ : w₁ ∈ ▲↑t
heq : i = 0
snd_eq✝ : j + 1 = 0
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
l₁ : w₁ ∈ ▲↑t
heq : i = 0
snd_eq✝ : j + 1 = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
x : ℕ
heq : (i, j + 1) = (Nat.succ x, 0)
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (x, j) }
⊢ False
Tactic:
injection heq with heq
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
x : ℕ
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (x, j) }
heq : i = Nat.succ x
snd_eq✝ : j + 1 = 0
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x✝ : Lex (ℕ × ℕ)
x : ℕ
l₁ : w₁ ∈ ▲{ f | ∃ j, f ∈ lindenbaumSequence t Δ (x, j) }
heq : i = Nat.succ x
snd_eq✝ : j + 1 = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
heq : (i, j + 1) = (n, Nat.succ m)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False
Tactic:
have l₃ := lindenbaumAvoids h₁ h₂ ⟨i,j⟩
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
heq : (i, j + 1) = (n, Nat.succ m)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
heq : (i, j + 1) = (n, Nat.succ m)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Tactic:
injection heq with heq₁ heq₂
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
heq₁ : i = n
heq₂ : j + 1 = Nat.succ m
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
heq₁ : i = n
heq₂ : j + 1 = Nat.succ m
⊢ False
Tactic:
injection heq₂ with heq₂
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
heq₁ : i = n
heq₂ : Nat.add j 0 = m
⊢ False