internlm/Lean-Github huggingface dataset:
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₂ : Nat.add j 0 = m
⊢ False
Tactic:
rw [←heq₁,←heq₂] 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₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i, Nat.add j 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).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
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 Δ (i, Nat.add j 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).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
Tactic:
clear n m x heq₁ heq₂ h₃
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i, Nat.add j 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).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 : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (i, Nat.add j 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add j 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Tactic:
dsimp at l₁ j
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲if
          (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
            ▲lindenbaumSequence t Δ (i, j + 0) then
        if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
          lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
        else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
      else lindenbaumSequence t Δ (i, j + 0)
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
l₁ :
  w₁ ∈
    ▲if
          (Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd ∈
            ▲lindenbaumSequence t Δ (i, j + 0) then
        if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
          lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
        else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
      else lindenbaumSequence t Δ (i, j + 0)
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
⊢ False
Tactic:
split at l₁
Proof state after:
case inl
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
l₁ :
  w₁ ∈
    ▲if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
        lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
      else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
⊢ False

case inr
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
l₁ : w₁ ∈ ▲lindenbaumSequence t Δ (i, j + 0)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
l₁ : w₁ ∈ ▲lindenbaumSequence t Δ (i, j + 0)
⊢ False
Tactic:
case inr h₄ => exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁, l₁, l₂⟩
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
l₁ :
  w₁ ∈
    ▲if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
        lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
      else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
⊢ False
Tactic:
case inl h₄ =>
  split at l₁
  case inl h₅ => exact (Set.not_nonempty_iff_eq_empty.mpr h₅) ⟨w₁, l₁, l₂⟩
  case inr h₅ =>
    have ⟨prf₁⟩ := l₁
    have ⟨w₂,⟨⟨prf₂⟩,l₄⟩⟩ := Set.nonempty_iff_ne_empty.mpr h₅
    have l₅ : w₁¦w₂ ∈ Δ := h₂ ⟨l₂, l₄⟩
    clear l₁ l₂ l₄ h₅
    have ⟨lst₁,l₆,prf₃⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₁)
    have ⟨lst₂,l₇,prf₄⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₂)
    have thm₁ := BTheorem.transitivity prf₃.toTheorem (BTheorem.orI₁ : BTheorem (w₁ ⊃ w₁ ¦ w₂))
    have thm₂ := BTheorem.transitivity prf₄.toTheorem (BTheorem.orI₂ : BTheorem (w₂ ⊃ w₁ ¦ w₂))
    have thm₃ := BTheorem.mp (BTheorem.adj thm₂ thm₁) BTheorem.orE 
    have ⟨prf₅⟩ := h₄
    clear h₄ thm₁ thm₂ prf₁ prf₂ prf₃ prf₄
    cases lst₁
    all_goals 
      cases lst₂
    case' nil.nil =>
      have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
      exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
    case' nil.cons head tail =>
      have := BProof.proveList l₇
      have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
      have := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
      have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
      exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
    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⟩
    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:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
l₁ : w₁ ∈ ▲lindenbaumSequence t Δ (i, j + 0)
⊢ False
Tactic:
exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁, l₁, l₂⟩
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
l₁ :
  w₁ ∈
    ▲if ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅ then
        lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}
      else lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}
⊢ False
Tactic:
split at l₁
Proof state after:
case inl
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h✝ : ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst})
⊢ False

case inr
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h✝ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(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₂ : w₁ ∈ Δ
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)
h₅ : ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst})
⊢ False
Tactic:
case inl h₅ => exact (Set.not_nonempty_iff_eq_empty.mpr h₅) ⟨w₁, l₁, l₂⟩
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
⊢ False
Tactic:
case inr h₅ =>
  have ⟨prf₁⟩ := l₁
  have ⟨w₂,⟨⟨prf₂⟩,l₄⟩⟩ := Set.nonempty_iff_ne_empty.mpr h₅
  have l₅ : w₁¦w₂ ∈ Δ := h₂ ⟨l₂, l₄⟩
  clear l₁ l₂ l₄ h₅
  have ⟨lst₁,l₆,prf₃⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₁)
  have ⟨lst₂,l₇,prf₄⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₂)
  have thm₁ := BTheorem.transitivity prf₃.toTheorem (BTheorem.orI₁ : BTheorem (w₁ ⊃ w₁ ¦ w₂))
  have thm₂ := BTheorem.transitivity prf₄.toTheorem (BTheorem.orI₂ : BTheorem (w₂ ⊃ w₁ ¦ w₂))
  have thm₃ := BTheorem.mp (BTheorem.adj thm₂ thm₁) BTheorem.orE 
  have ⟨prf₅⟩ := h₄
  clear h₄ thm₁ thm₂ prf₁ prf₂ prf₃ prf₄
  cases lst₁
  all_goals 
    cases lst₂
  case' nil.nil =>
    have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
    exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
  case' nil.cons head tail =>
    have := BProof.proveList l₇
    have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
    have := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
    have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
    exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
  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⟩
  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:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h₅ : ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst})
⊢ False
Tactic:
exact (Set.not_nonempty_iff_eq_empty.mpr h₅) ⟨w₁, l₁, l₂⟩
Proof state after:
no goals
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
⊢ False
Tactic:
have ⟨prf₁⟩ := l₁
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
prf₁ : BProof (lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd}) w₁
⊢ False
Tactic:
have ⟨w₂,⟨⟨prf₂⟩,l₄⟩⟩ := Set.nonempty_iff_ne_empty.mpr h₅
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
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₂ ∈ Δ
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
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₂ ∈ Δ
⊢ False
Tactic:
have l₅ : w₁¦w₂ ∈ Δ := h₂ ⟨l₂, l₄⟩
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
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₂ ∈ Δ
l₅ : w₁¦w₂ ∈ Δ
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₂ : w₁ ∈ Δ
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)
h₅ : ¬▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).fst}) ∩ Δ = ∅
l₁ : w₁ ∈ ▲(lindenbaumSequence t Δ (i, j + 0) ∪ {(Denumerable.ofNat (Form × Form) (j + 0)).snd})
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₂ ∈ Δ
l₅ : w₁¦w₂ ∈ Δ
⊢ False
Tactic:
clear l₁ l₂ l₄ 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₂ ∈ Δ
⊢ 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₂ ∈ Δ
⊢ False
Tactic:
have ⟨lst₁,l₆,prf₃⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₁)
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₁
⊢ 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₁
⊢ False
Tactic:
have ⟨lst₂,l₇,prf₄⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₂)
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₂
⊢ False