Theorem: lindenbaumIsFormal (Fine/SystemB/Lindenbaum.lean)

State before:
t : Th
Δ : Ctx
⊢ formalTheory (lindenbaumExtension t Δ)
Tactic:
intros f
State after:
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ ↔ lindenbaumExtension t Δ⊢f

State before:
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ ↔ lindenbaumExtension t Δ⊢f
Tactic:
apply Iff.intro
State after:
case mp
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ → lindenbaumExtension t Δ⊢f

case mpr
t : Th
Δ : Ctx
f : Form
⊢ lindenbaumExtension t Δ⊢f → f ∈ lindenbaumExtension t Δ

State before:
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ → lindenbaumExtension t Δ⊢f
Tactic:
case mp =>
  intro h₁
  exact ⟨BProof.ax h₁⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
f : Form
⊢ lindenbaumExtension t Δ⊢f → f ∈ lindenbaumExtension t Δ
Tactic:
case mpr =>
  intro h₁
  have ⟨prf₁⟩ := h₁
  have ⟨s, l₁, fprf⟩ := BProof.compactness prf₁
  have ⟨⟨i,j⟩,l₂⟩ := finiteExhaustion lindenbaumSequenceMonotone l₁
  have l₃ : lindenbaumSequence t Δ ⟨i,j⟩ ⊆ lindenbaumSequence t Δ ⟨i + 1,Encodable.encode (f,f)⟩ := by
    apply lindenbaumSequenceMonotone
    apply (Prod.Lex.le_iff (i,j) (i + 1,Encodable.encode (f,f))).mpr $ Or.inl $ Nat.lt_succ_self i
  have prf₂ := BProof.monotone (le_trans l₂ l₃) fprf
  have prf₃ : BProof (lindenbaumSequence t Δ ⟨i+1,Encodable.encode (f,f)⟩) (f ¦ f) := BProof.mp prf₂ BTheorem.orI₁
  clear s h₁ l₁ l₂ l₃ fprf prf₁ prf₂ 
  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₇
  exact ⟨⟨i + 1, Encodable.encode (f,f) + 1⟩, l₄⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ → lindenbaumExtension t Δ⊢f
Tactic:
intro h₁
State after:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ lindenbaumExtension t Δ
⊢ lindenbaumExtension t Δ⊢f

State before:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ lindenbaumExtension t Δ
⊢ lindenbaumExtension t Δ⊢f
Tactic:
exact ⟨BProof.ax h₁⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
f : Form
⊢ lindenbaumExtension t Δ⊢f → f ∈ lindenbaumExtension t Δ
Tactic:
intro h₁
State after:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
⊢ f ∈ lindenbaumExtension t Δ

State before:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
have ⟨prf₁⟩ := h₁
State after:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
⊢ f ∈ lindenbaumExtension t Δ

State before:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
have ⟨s, l₁, fprf⟩ := BProof.compactness prf₁
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
⊢ f ∈ lindenbaumExtension t Δ

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
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
have ⟨⟨i,j⟩,l₂⟩ := finiteExhaustion lindenbaumSequenceMonotone l₁
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)
⊢ f ∈ lindenbaumExtension t Δ

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)
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
have l₃ : lindenbaumSequence t Δ ⟨i,j⟩ ⊆ lindenbaumSequence t Δ ⟨i + 1,Encodable.encode (f,f)⟩ := by
  apply lindenbaumSequenceMonotone
  apply (Prod.Lex.le_iff (i,j) (i + 1,Encodable.encode (f,f))).mpr $ Or.inl $ Nat.lt_succ_self i
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))
⊢ f ∈ lindenbaumExtension t Δ

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

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

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₂
State after:
t : Th
Δ : Ctx
f : Form
i j : ℕ
prf₃ : BProof (lindenbaumSequence t Δ (i + 1, Encodable.encode (f, f))) (f¦f)
⊢ f ∈ lindenbaumExtension t Δ

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

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₄⟩
State after:
no goals

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

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
State after:
no goals

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

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

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

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

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

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

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
State after:
no goals

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₇
State after:
no goals

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

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)]
State after:
no goals

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

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)]
State after:
no goals

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

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

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
State after:
no goals

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

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

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

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₇
State after:
no goals