internlm/Lean-Github huggingface dataset:
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
⊢ f ∈
    let prev := lindenbaumSequence t Δ (i, j);
    let l := (Denumerable.ofNat (Form × Form) j).fst;
    let r := (Denumerable.ofNat (Form × Form) j).snd;
    if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Tactic:
change
  let prev := lindenbaumSequence t Δ (i, j);
  let l := (Denumerable.ofNat (Form × Form) j).fst;
  let r := (Denumerable.ofNat (Form × Form) j).snd;
  f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
⊢ let prev := lindenbaumSequence t Δ (i, j);
  let l := (Denumerable.ofNat (Form × Form) j).fst;
  let r := (Denumerable.ofNat (Form × Form) j).snd;
  f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
⊢ let prev := lindenbaumSequence t Δ (i, j);
  let l := (Denumerable.ofNat (Form × Form) j).fst;
  let r := (Denumerable.ofNat (Form × Form) j).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
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
⊢ f ∈ if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
⊢ 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
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝ : l¦r ∈ ▲prev
⊢ f ∈ if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r}

case inr
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝ : ¬l¦r ∈ ▲prev
⊢ f ∈ prev
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝ : l¦r ∈ ▲prev
⊢ f ∈ if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r}
Tactic:
case inl =>
  split
  case inl | inr => apply Or.inl h₃
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝ : ¬l¦r ∈ ▲prev
⊢ f ∈ prev
Tactic:
case inr => exact h₃
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝ : l¦r ∈ ▲prev
⊢ f ∈ if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r}
Tactic:
split
Proof state after:
case inl
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝¹ : l¦r ∈ ▲prev
h✝ : ▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {l}

case inr
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝¹ : l¦r ∈ ▲prev
h✝ : ¬▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {r}
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝¹ : l¦r ∈ ▲prev
h✝ : ¬▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {r}
Tactic:
case inl | inr => apply Or.inl h₃
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝¹ : l¦r ∈ ▲prev
h✝ : ¬▲(prev ∪ {l}) ∩ Δ = ∅
⊢ f ∈ prev ∪ {r}
Tactic:
apply Or.inl h₃
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq₁ : i = i'
heq₂ : Nat.add j 0 = j'
heq₃ : j = j'
prev : Ctx := lindenbaumSequence t Δ (i, j)
l : Form := (Denumerable.ofNat (Form × Form) j).fst
r : Form := (Denumerable.ofNat (Form × Form) j).snd
h✝ : ¬l¦r ∈ ▲prev
⊢ f ∈ prev
Tactic:
exact h₃
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
have l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j := Or.inl h₂
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
have l₂ := (Prod.Lex.le_iff (a₁, b₁) (i,j)).mpr l₁
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j
l₂ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, j)
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j
l₂ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, j)
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
have l₃ := @lindenbaumSequenceMonotone' t Δ (i,j) (a₁, b₁)  l₂
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j
l₂ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, j)
l₃ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j)
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j
l₂ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, j)
l₃ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j)
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
apply le_trans l₃
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j
l₂ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, j)
l₃ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j)
⊢ lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a₁ b₁ : ℕ
h₂ : a₁ < i
l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j
l₂ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, j)
l₃ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, j)
⊢ lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
Tactic:
exact lem
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : b₁ ≤ j + 1
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
cases h₂
Proof state after:
case refl
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
⊢ lindenbaumSequence t Δ (i, j + 1) ⊆ lindenbaumSequence t Δ (i, j + 1)

case step
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
a✝ : Nat.le b₁ (Nat.add j 0)
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
⊢ lindenbaumSequence t Δ (i, j + 1) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
case refl => intros _ h₁; assumption
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : Nat.le b₁ (Nat.add j 0)
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
case step h₂ =>
  have l₁ : i < i ∨ i = i ∧ b₁ ≤ j := Or.inr ⟨rfl, h₂⟩
  have l₂ := (Prod.Lex.le_iff (i, b₁) (i,j)).mpr l₁
  have l₃ := @lindenbaumSequenceMonotone' t Δ (i,j) (i, b₁)  l₂
  apply le_trans l₃
  exact lem
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
⊢ lindenbaumSequence t Δ (i, j + 1) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
intros _ h₁
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a✝ : Form
h₁ : a✝ ∈ lindenbaumSequence t Δ (i, j + 1)
⊢ a✝ ∈ lindenbaumSequence t Δ (i, j + 1)
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a✝ : Form
h₁ : a✝ ∈ lindenbaumSequence t Δ (i, j + 1)
⊢ a✝ ∈ lindenbaumSequence t Δ (i, j + 1)
Tactic:
assumption
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : Nat.le b₁ (Nat.add j 0)
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
have l₁ : i < i ∨ i = i ∧ b₁ ≤ j := Or.inr ⟨rfl, h₂⟩
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : Nat.le b₁ (Nat.add j 0)
l₁ : i < i ∨ i = i ∧ b₁ ≤ j
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : Nat.le b₁ (Nat.add j 0)
l₁ : i < i ∨ i = i ∧ b₁ ≤ j
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
have l₂ := (Prod.Lex.le_iff (i, b₁) (i,j)).mpr l₁
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : Nat.le b₁ (Nat.add j 0)
l₁ : i < i ∨ i = i ∧ b₁ ≤ j
l₂ : ↑toLex (i, b₁) ≤ ↑toLex (i, j)
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : Nat.le b₁ (Nat.add j 0)
l₁ : i < i ∨ i = i ∧ b₁ ≤ j
l₂ : ↑toLex (i, b₁) ≤ ↑toLex (i, j)
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
have l₃ := @lindenbaumSequenceMonotone' t Δ (i,j) (i, b₁)  l₂
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : Nat.le b₁ (Nat.add j 0)
l₁ : i < i ∨ i = i ∧ b₁ ≤ j
l₂ : ↑toLex (i, b₁) ≤ ↑toLex (i, j)
l₃ : lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j)
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : Nat.le b₁ (Nat.add j 0)
l₁ : i < i ∨ i = i ∧ b₁ ≤ j
l₂ : ↑toLex (i, b₁) ≤ ↑toLex (i, j)
l₃ : lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j)
⊢ lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
apply le_trans l₃
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : Nat.le b₁ (Nat.add j 0)
l₁ : i < i ∨ i = i ∧ b₁ ≤ j
l₂ : ↑toLex (i, b₁) ≤ ↑toLex (i, j)
l₃ : lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j)
⊢ lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
b₁ : ℕ
h₂ : Nat.le b₁ (Nat.add j 0)
l₁ : i < i ∨ i = i ∧ b₁ ≤ j
l₂ : ↑toLex (i, b₁) ≤ ↑toLex (i, j)
l₃ : lindenbaumSequence t Δ (i, b₁) ⊆ lindenbaumSequence t Δ (i, j)
⊢ lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
Tactic:
exact lem
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone
Proof state before:
t : Th
Δ : Ctx
⊢ Monotone (lindenbaumSequence t Δ)
Tactic:
intros a b
Proof state after:
t : Th
Δ : Ctx
a b : Lex (ℕ × ℕ)
⊢ a ≤ b → lindenbaumSequence t Δ a ≤ lindenbaumSequence t Δ b
Theorem: lindenbaumSequenceMonotone
Proof state before:
t : Th
Δ : Ctx
a b : Lex (ℕ × ℕ)
⊢ a ≤ b → lindenbaumSequence t Δ a ≤ lindenbaumSequence t Δ b
Tactic:
exact lindenbaumSequenceMonotone' b a
Proof state after:
no goals
Theorem: lindenbaumStageMonotone
Proof state before:
t : Th
Δ : Ctx
i : ℕ
⊢ Monotone fun j => lindenbaumSequence t Δ (i, j)
Tactic:
intros a b h₁
Proof state after:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
⊢ (fun j => lindenbaumSequence t Δ (i, j)) a ≤ (fun j => lindenbaumSequence t Δ (i, j)) b
Theorem: lindenbaumStageMonotone
Proof state before:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
⊢ (fun j => lindenbaumSequence t Δ (i, j)) a ≤ (fun j => lindenbaumSequence t Δ (i, j)) b
Tactic:
change lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)
Proof state after:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
⊢ lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)
Theorem: lindenbaumStageMonotone
Proof state before:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
⊢ lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)
Tactic:
have l₂ := (Prod.Lex.le_iff (i, a) (i,b)).mpr $ Or.inr ⟨rfl,h₁⟩
Proof state after:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
l₂ : ↑toLex (i, a) ≤ ↑toLex (i, b)
⊢ lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)
Theorem: lindenbaumStageMonotone
Proof state before:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
l₂ : ↑toLex (i, a) ≤ ↑toLex (i, b)
⊢ lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)
Tactic:
exact lindenbaumSequenceMonotone' (i,b) (i,a) l₂
Proof state after:
no goals
Theorem: lindenbaumExtensionExtends
Proof state before:
t : Th
Δ : Ctx
⊢ ↑t ⊆ lindenbaumExtension t Δ
Tactic:
intros f h₁
Proof state after:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ ↑t
⊢ f ∈ lindenbaumExtension t Δ
Theorem: lindenbaumExtensionExtends
Proof state before:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ ↑t
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
refine ⟨⟨0,0⟩,?_⟩
Proof state after:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ ↑t
⊢ f ∈ lindenbaumSequence t Δ (0, 0)
Theorem: lindenbaumExtensionExtends
Proof state before:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ ↑t
⊢ f ∈ lindenbaumSequence t Δ (0, 0)
Tactic:
assumption
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
⊢ formalTheory (lindenbaumExtension t Δ)
Tactic:
intros f
Proof state after:
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ ↔ lindenbaumExtension t Δ⊢f
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ ↔ lindenbaumExtension t Δ⊢f
Tactic:
apply Iff.intro
Proof 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 Δ
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ → lindenbaumExtension t Δ⊢f
Tactic:
case mp =>
  intro h₁
  exact ⟨BProof.ax h₁⟩
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof 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₄⟩
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
⊢ f ∈ lindenbaumExtension t Δ → lindenbaumExtension t Δ⊢f
Tactic:
intro h₁
Proof state after:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ lindenbaumExtension t Δ
⊢ lindenbaumExtension t Δ⊢f
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
h₁ : f ∈ lindenbaumExtension t Δ
⊢ lindenbaumExtension t Δ⊢f
Tactic:
exact ⟨BProof.ax h₁⟩
Proof state after:
no goals
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
⊢ lindenbaumExtension t Δ⊢f → f ∈ lindenbaumExtension t Δ
Tactic:
intro h₁
Proof state after:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
⊢ f ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsFormal
Proof state before:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
have ⟨prf₁⟩ := h₁
Proof state after:
t : Th
Δ : Ctx
f : Form
h₁ : lindenbaumExtension t Δ⊢f
prf₁ : BProof (lindenbaumExtension t Δ) f
⊢ f ∈ lindenbaumExtension t Δ
Theorem: lindenbaumIsFormal
Proof 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₁
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
⊢ 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
⊢ f ∈ lindenbaumExtension t Δ
Tactic:
have ⟨⟨i,j⟩,l₂⟩ := finiteExhaustion lindenbaumSequenceMonotone l₁
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)
⊢ 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)
⊢ 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
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))
⊢ f ∈ lindenbaumExtension t Δ