internlm/Lean-Github huggingface dataset:
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₃ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
have prf₂ := BProof.monotone (le_trans l₂ l₃) fprf
Proof state after:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₃ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
prf₂ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) f
⊢ f ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₃ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
prf₂ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) f
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
have prf₃ : BProof (lindenbaumSequence t Δ ⟨i+1,Encodable.encode (f,f)⟩) (f ¦ f) := BProof.mp prf₂ BTheorem.orI₁
Proof state after:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₃ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
prf₂ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) f
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ f ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
l₃ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
prf₂ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) f
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
clear s h₁ l₁ l₂ l₃ fprf prf₁ prf₂
Proof state after:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ f ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
have l₄ : f ∈ lindenbaumSequence t Δ ⟨i + 1, Encodable.encode (f,f) + 1⟩ := by
  unfold lindenbaumSequence
  change
    let prev := lindenbaumSequence t Δ (i + 1, Encodable.encode (f,f));
    let l := (Denumerable.ofNat (Form × Form) (Encodable.encode (f,f))).fst;
    let r := (Denumerable.ofNat (Form × Form) (Encodable.encode (f,f))).snd;
    f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
  intros prev l r
  have l₅ : l = f := by 
    change (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst = f
    rw [Denumerable.ofNat_encode (f,f)]
  have l₆ : r = f := by
    change (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd = f
    rw [Denumerable.ofNat_encode (f,f)]
  split
  case inl h₂ =>
    split
    . rw [l₅]; exact Or.inr rfl
    . rw [l₆]; exact Or.inr rfl
  case inr h₂ =>
    apply False.elim
    have l₇ : f¦f ∈ ▲prev := ⟨prf₃⟩
    rw [l₅,l₆] at h₂
    exact h₂ l₇
Proof state after:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
l₄ : f ∈ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f) + 1)
⊢ f ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
l₄ : f ∈ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f) + 1)
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
exact ⟨⟨i + 1, Encodable.encode (f,f) + 1⟩, l₄⟩
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
⊢ lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
Tactic:
apply lindenbaumSequenceMonotone
Proof state after:
case a
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
⊢ (i, j) ≤ (i + 1, Encodable.encode (f, f))
Theorem: lindenbaumIsFormal
Proof state before:
case a
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
s : Finset Form
l₁ : ↑s ⊆ lindenbaumExtension t Δ
fprf : BProof (↑s) f
i j : ℕ
l₂ : ↑s ⊆ lindenbaumSequence t Δ (i, j)
⊢ (i, j) ≤ (i + 1, Encodable.encode (f, f))
Tactic:
apply (Prod.Lex.le_iff (i,j) (i + 1,Encodable.encode (f,f))).mpr $ Or.inl $ Nat.lt_succ_self i
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ f ∈ lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f) + 1)
Tactic:
unfold lindenbaumSequence
Proof state after:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ f ∈
    let prev := lindenbaumSequence t Δ (Nat.succ (Nat.add i 0), Nat.add (Encodable.encode (f, f)) 0);
    let l := (Denumerable.ofNat (Form × Form) (Nat.add (Encodable.encode (f, f)) 0)).fst;
    let r := (Denumerable.ofNat (Form × Form) (Nat.add (Encodable.encode (f, f)) 0)).snd;
    if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ f ∈
    let prev := lindenbaumSequence t Δ (Nat.succ (Nat.add i 0), Nat.add (Encodable.encode (f, f)) 0);
    let l := (Denumerable.ofNat (Form × Form) (Nat.add (Encodable.encode (f, f)) 0)).fst;
    let r := (Denumerable.ofNat (Form × Form) (Nat.add (Encodable.encode (f, f)) 0)).snd;
    if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Tactic:
change
  let prev := lindenbaumSequence t Δ (i + 1, Encodable.encode (f,f));
  let l := (Denumerable.ofNat (Form × Form) (Encodable.encode (f,f))).fst;
  let r := (Denumerable.ofNat (Form × Form) (Encodable.encode (f,f))).snd;
  f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Proof state after:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ let prev := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f));
  let l := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst;
  let r := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd;
  f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ let prev := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f));
  let l := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst;
  let r := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd;
  f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Tactic:
intros prev l r
Proof state after:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
⊢ f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
⊢ f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Tactic:
have l₅ : l = f := by 
  change (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst = f
  rw [Denumerable.ofNat_encode (f,f)]
Proof state after:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
⊢ f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
⊢ f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Tactic:
have l₆ : r = f := by
  change (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd = f
  rw [Denumerable.ofNat_encode (f,f)]
Proof state after:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
⊢ f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
⊢ f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Tactic:
split
Proof state after:
case inl
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h✝ : l¦r ∈ ▲prev
⊢ f ∈ if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r}

case inr
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h✝ : ¬l¦r ∈ ▲prev
⊢ f ∈ prev
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
⊢ f ∈ if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r}
Tactic:
case inl h₂ =>
  split
  . rw [l₅]; exact Or.inr rfl
  . rw [l₆]; exact Or.inr rfl
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : ¬l¦r ∈ ▲prev
⊢ f ∈ prev
Tactic:
case inr h₂ =>
  apply False.elim
  have l₇ : f¦f ∈ ▲prev := ⟨prf₃⟩
  rw [l₅,l₆] at h₂
  exact h₂ l₇
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
⊢ l = f
Tactic:
change (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst = f
Proof state after:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
⊢ (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst = f
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
⊢ (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst = f
Tactic:
rw [Denumerable.ofNat_encode (f,f)]
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
⊢ r = f
Tactic:
change (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd = f
Proof state after:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
⊢ (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd = f
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
⊢ (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd = f
Tactic:
rw [Denumerable.ofNat_encode (f,f)]
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
⊢ f ∈ if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r}
Tactic:
split
Proof state after:
case inl
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
h✝ : ▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {l}

case inr
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
h✝ : ¬▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {r}
Theorem: lindenbaumIsFormal
Proof state before:
case inl
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
h✝ : ▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {l}

case inr
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
h✝ : ¬▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {r}
Tactic:
. rw [l₅]; exact Or.inr rfl
Proof state after:
case inr
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
h✝ : ¬▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {r}
Theorem: lindenbaumIsFormal
Proof state before:
case inr
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : l¦r ∈ ▲prev
h✝ : ¬▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {r}
Tactic:
. rw [l₆]; exact Or.inr rfl
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : ¬l¦r ∈ ▲prev
⊢ f ∈ prev
Tactic:
apply False.elim
Proof state after:
case h
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : ¬l¦r ∈ ▲prev
⊢ False
Theorem: lindenbaumIsFormal
Proof state before:
case h
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : ¬l¦r ∈ ▲prev
⊢ False
Tactic:
have l₇ : f¦f ∈ ▲prev := ⟨prf₃⟩
Proof state after:
case h
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : ¬l¦r ∈ ▲prev
l₇ : f¦f ∈ ▲prev
⊢ False
Theorem: lindenbaumIsFormal
Proof state before:
case h
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : ¬l¦r ∈ ▲prev
l₇ : f¦f ∈ ▲prev
⊢ False
Tactic:
rw [l₅,l₆] at h₂
Proof state after:
case h
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : ¬f¦f ∈ ▲prev
l₇ : f¦f ∈ ▲prev
⊢ False
Theorem: lindenbaumIsFormal
Proof state before:
case h
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
prev : Ctx := lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))
l : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).fst
r : Form := (Denumerable.ofNat (Form × Form) (Encodable.encode (f, f))).snd
l₅ : l = f
l₆ : r = f
h₂ : ¬f¦f ∈ ▲prev
l₇ : f¦f ∈ ▲prev
⊢ False
Tactic:
exact h₂ l₇
Proof state after:
no goals
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
⊢ isPrimeTheory (lindenbaumExtension t Δ)
Tactic:
intros f g h₁
Proof state after:
t : Th
Δ : Ctx
f g : Form
h₁ : f¦g ∈ lindenbaumExtension t Δ
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
h₁ : f¦g ∈ lindenbaumExtension t Δ
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
have ⟨⟨i,j⟩,h₂⟩ := h₁
Proof state after:
t : Th
Δ : Ctx
f g : Form
h₁ : f¦g ∈ lindenbaumExtension t Δ
i j : ℕ
h₂ : f¦g ∈ lindenbaumSequence t Δ (i, j)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
h₁ : f¦g ∈ lindenbaumExtension t Δ
i j : ℕ
h₂ : f¦g ∈ lindenbaumSequence t Δ (i, j)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
let k := Encodable.encode (f,g)
Proof state after:
t : Th
Δ : Ctx
f g : Form
h₁ : f¦g ∈ lindenbaumExtension t Δ
i j : ℕ
h₂ : f¦g ∈ lindenbaumSequence t Δ (i, j)
k : ℕ := Encodable.encode (f, g)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsPrime
Proof state before:
t : Th
Δ : Ctx
f g : Form
h₁ : f¦g ∈ lindenbaumExtension t Δ
i j : ℕ
h₂ : f¦g ∈ lindenbaumSequence t Δ (i, j)
k : ℕ := Encodable.encode (f, g)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
have l₁ : lindenbaumSequence t Δ ⟨i,j⟩ ⊆ lindenbaumSequence t Δ ⟨i + 1,k⟩ := by
  apply lindenbaumSequenceMonotone
  apply (Prod.Lex.le_iff (i,j) (i + 1,k)).mpr $ Or.inl $ Nat.lt_succ_self i
Proof state after:
t : Th
Δ : Ctx
f g : Form
h₁ : f¦g ∈ lindenbaumExtension t Δ
i j : ℕ
h₂ : f¦g ∈ lindenbaumSequence t Δ (i, j)
k : ℕ := Encodable.encode (f, g)
l₁ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, k)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ