internlm/Lean-Github huggingface dataset:
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)
l₁ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, k)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
have l₂ : f ¦ g ∈ lindenbaumSequence t Δ ⟨i + 1, k⟩ := l₁ h₂
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)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
⊢ 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)
l₁ : lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, k)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
clear l₁ h₁ 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)
⊢ 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)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
have l₃ : f ∈ lindenbaumSequence t Δ ⟨i + 1, k + 1⟩ ∨ g ∈ lindenbaumSequence t Δ ⟨i + 1, k + 1⟩ := by
  unfold lindenbaumSequence
  change
    let prev := lindenbaumSequence t Δ (i + 1, k);
    let l := (Denumerable.ofNat (Form × Form) k).fst;
    let r := (Denumerable.ofNat (Form × Form) k).snd;
    (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨ 
    (g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev)
  intros prev l r
  have l₄ : Denumerable.ofNat (Form × Form) k = (f,g) := Denumerable.ofNat_encode (f,g)
  have l₅ : l = f := by 
    change (Denumerable.ofNat (Form × Form) k).fst = f
    rw [l₄]
  have l₆ : r = g := by 
    change (Denumerable.ofNat (Form × Form) k).snd = g
    rw [l₄]
  repeat rw [l₅,l₆]
  clear l r l₅ l₆
  cases Classical.em (▲(prev ∪ {f}) ∩ Δ = ∅)
  case' inl h₁ => apply Or.inl
  case' inr h₁ => apply Or.inr
  all_goals
    split
    case inl => exact Or.inr rfl
    case inr h₂ => exact False.elim $ h₂ ⟨BProof.ax l₂⟩
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)
⊢ 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)
⊢ f ∈ lindenbaumExtension t Δ ∨ g ∈ lindenbaumExtension t Δ
Tactic:
apply Or.elim l₃
Proof state after:
case left
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 Δ

case right
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 Δ
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:
case left => intros h₁; 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:
case right => intros h₁; exact Or.inr ⟨⟨i+1,k+1⟩,h₁⟩
Proof state after:
no goals
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)
⊢ lindenbaumSequence t Δ (i, j) ⊆ lindenbaumSequence t Δ (i + 1, k)
Tactic:
apply lindenbaumSequenceMonotone
Proof state after:
case a
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)
⊢ (i, j) ≤ (i + 1, k)
Theorem: lindenbaumIsPrime
Proof state before:
case a
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)
⊢ (i, j) ≤ (i + 1, k)
Tactic:
apply (Prod.Lex.le_iff (i,j) (i + 1,k)).mpr $ Or.inl $ Nat.lt_succ_self i
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)
⊢ f ∈ lindenbaumSequence t Δ (i + 1, k + 1) ∨ g ∈ lindenbaumSequence t Δ (i + 1, k + 1)
Tactic:
unfold lindenbaumSequence
Proof state after:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
⊢ (f ∈
      let prev := lindenbaumSequence t Δ (Nat.succ (Nat.add i 0), Nat.add k 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈
      let prev := lindenbaumSequence t Δ (Nat.succ (Nat.add i 0), Nat.add k 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else 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)
⊢ (f ∈
      let prev := lindenbaumSequence t Δ (Nat.succ (Nat.add i 0), Nat.add k 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈
      let prev := lindenbaumSequence t Δ (Nat.succ (Nat.add i 0), Nat.add k 0);
      let l := (Denumerable.ofNat (Form × Form) (Nat.add k 0)).fst;
      let r := (Denumerable.ofNat (Form × Form) (Nat.add k 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, k);
  let l := (Denumerable.ofNat (Form × Form) k).fst;
  let r := (Denumerable.ofNat (Form × Form) k).snd;
  (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨ 
  (g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev)
Proof state after:
t : Th
Δ : Ctx
f g : Form
i j : ℕ
k : ℕ := Encodable.encode (f, g)
l₂ : f¦g ∈ lindenbaumSequence t Δ (i + 1, k)
⊢ let prev := lindenbaumSequence t Δ (i + 1, k);
  let l := (Denumerable.ofNat (Form × Form) k).fst;
  let r := (Denumerable.ofNat (Form × Form) k).snd;
  (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else 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)
⊢ let prev := lindenbaumSequence t Δ (i + 1, k);
  let l := (Denumerable.ofNat (Form × Form) k).fst;
  let r := (Denumerable.ofNat (Form × Form) k).snd;
  (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ 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 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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else 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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Tactic:
have l₄ : Denumerable.ofNat (Form × Form) k = (f,g) := Denumerable.ofNat_encode (f,g)
Proof state after:
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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else 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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ 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) k).fst = f
  rw [l₄]
Proof state after:
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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else 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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Tactic:
have l₆ : r = g := by 
  change (Denumerable.ofNat (Form × Form) k).snd = g
  rw [l₄]
Proof state after:
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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
l₆ : r = g
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else 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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
l₆ : r = g
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Tactic:
repeat rw [l₅,l₆]
Proof state after:
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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
l₆ : r = g
⊢ (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
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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
l₆ : r = g
⊢ (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:
clear l r l₅ l₆
Proof state after:
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)
⊢ (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
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)
⊢ (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:
cases Classical.em (▲(prev ∪ {f}) ∩ Δ = ∅)
Proof state after:
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

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
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

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:
case' inl h₁ => apply Or.inl
Proof state after:
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

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
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

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:
case' inr h₁ => apply Or.inr
Proof state after:
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}) ∩ Δ = ∅
⊢ g ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev

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
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}) ∩ Δ = ∅
⊢ g ∈ if f¦g ∈ ▲prev then if ▲(prev ∪ {f}) ∩ Δ = ∅ then prev ∪ {f} else prev ∪ {g} else prev

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:
all_goals
  split
  case inl => exact Or.inr rfl
  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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
⊢ l = f
Tactic:
change (Denumerable.ofNat (Form × Form) k).fst = f
Proof state after:
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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
⊢ (Denumerable.ofNat (Form × Form) k).fst = f
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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
⊢ (Denumerable.ofNat (Form × Form) k).fst = f
Tactic:
rw [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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
⊢ r = g
Tactic:
change (Denumerable.ofNat (Form × Form) k).snd = g
Proof state after:
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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
⊢ (Denumerable.ofNat (Form × Form) k).snd = g
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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
⊢ (Denumerable.ofNat (Form × Form) k).snd = g
Tactic:
rw [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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
l₆ : r = g
⊢ (f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev) ∨
    g ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Tactic:
rw [l₅,l₆]
Proof state after:
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 : Form := (Denumerable.ofNat (Form × Form) k).fst
r : Form := (Denumerable.ofNat (Form × Form) k).snd
l₄ : Denumerable.ofNat (Form × Form) k = (f, g)
l₅ : l = f
l₆ : r = g
⊢ (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