Theorem: lindenbaumSequenceMonotone' (Fine/SystemB/Lindenbaum.lean)

State before:
t : Th
Δ : Ctx
⊢ ∀ (b a : Lex (ℕ × ℕ)), a ≤ b → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ b
Tactic:
intros b
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ b → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ b

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ b → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ b
Tactic:
match b with
  | ⟨0, 0⟩ =>
    intros a h₁
    cases h₁
    case left a₁ _ h₂ => exact False.elim $ Nat.not_lt_zero a₁ h₂
    case right b₁ h₂ =>
      rw [Nat.le_zero_eq b₁] at h₂
      rw [h₂]
  | ⟨i + 1, 0⟩ =>
    intros a h₁
    cases h₁
    case left a₁ b₁ h₂ => 
      have l₁ : a₁ < i ∨ a₁ = i := Nat.lt_or_eq_of_le $ Nat.lt_succ.mp h₂
      have l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁ := by 
        cases l₁
        case inl h₂ => exact Or.inl h₂
        case inr h₂ => exact Or.inr ⟨h₂, le_refl b₁⟩
      have l₃ := (Prod.Lex.le_iff (a₁, b₁) (i,b₁)).mpr l₂
      have l₄ := @lindenbaumSequenceMonotone' t Δ (i,b₁) (a₁, b₁) l₃
      apply le_trans l₄
      intros f h₂
      exact ⟨b₁,h₂⟩
    case right b₁ h₂ =>
      rw [Nat.le_zero_eq b₁] at h₂
      rw [h₂]
  | ⟨i, j + 1⟩ =>
    have lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1) := by
      intros f h₃
      unfold lindenbaumSequence
      split
      case h_1 _ heq | h_2 _ heq => injection heq; contradiction
      case h_3 i' j' heq =>
        injection heq with heq₁ heq₂
        injection heq₂ with heq₂
        have heq₃ : j = j' := heq₂
        rw [←heq₁, ←heq₃]
        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
        intros prev l r
        split
        case inl =>
          split
          case inl | inr => apply Or.inl h₃
        case inr => exact h₃
    intros a h₁
    cases h₁
    case left a₁ b₁ h₂ =>
        have l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j := Or.inl h₂
        have l₂ := (Prod.Lex.le_iff (a₁, b₁) (i,j)).mpr l₁
        have l₃ := @lindenbaumSequenceMonotone' t Δ (i,j) (a₁, b₁)  l₂
        apply le_trans l₃
        exact lem
    case right b₁ h₂ =>
      cases h₂
      case refl => intros _ h₁; assumption
      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
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ (0, 0) → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (0, 0)
Tactic:
intros a h₁
State after:
t : Th
Δ : Ctx
b a : Lex (ℕ × ℕ)
h₁ : a ≤ (0, 0)
⊢ lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (0, 0)

State before:
t : Th
Δ : Ctx
b a : Lex (ℕ × ℕ)
h₁ : a ≤ (0, 0)
⊢ lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (0, 0)
Tactic:
cases h₁
State after:
case left
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
a₁✝ b₁✝ : ℕ
h✝ : a₁✝ < 0
⊢ lindenbaumSequence t Δ (a₁✝, b₁✝) ⊆ lindenbaumSequence t Δ (0, 0)

case right
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
b₁✝ : ℕ
h✝ : b₁✝ ≤ 0
⊢ lindenbaumSequence t Δ (0, b₁✝) ⊆ lindenbaumSequence t Δ (0, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
a₁ b₁✝ : ℕ
h₂ : a₁ < 0
⊢ lindenbaumSequence t Δ (a₁, b₁✝) ⊆ lindenbaumSequence t Δ (0, 0)
Tactic:
case left a₁ _ h₂ => exact False.elim $ Nat.not_lt_zero a₁ h₂
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
b₁ : ℕ
h₂ : b₁ ≤ 0
⊢ lindenbaumSequence t Δ (0, b₁) ⊆ lindenbaumSequence t Δ (0, 0)
Tactic:
case right b₁ h₂ =>
  rw [Nat.le_zero_eq b₁] at h₂
  rw [h₂]
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
a₁ b₁✝ : ℕ
h₂ : a₁ < 0
⊢ lindenbaumSequence t Δ (a₁, b₁✝) ⊆ lindenbaumSequence t Δ (0, 0)
Tactic:
exact False.elim $ Nat.not_lt_zero a₁ h₂
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
b₁ : ℕ
h₂ : b₁ ≤ 0
⊢ lindenbaumSequence t Δ (0, b₁) ⊆ lindenbaumSequence t Δ (0, 0)
Tactic:
rw [Nat.le_zero_eq b₁] at h₂
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
b₁ : ℕ
h₂ : b₁ = 0
⊢ lindenbaumSequence t Δ (0, b₁) ⊆ lindenbaumSequence t Δ (0, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
b₁ : ℕ
h₂ : b₁ = 0
⊢ lindenbaumSequence t Δ (0, b₁) ⊆ lindenbaumSequence t Δ (0, 0)
Tactic:
rw [h₂]
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i : ℕ
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ (i + 1, 0) → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
intros a h₁
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i : ℕ
a : Lex (ℕ × ℕ)
h₁ : a ≤ (i + 1, 0)
⊢ lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i + 1, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i : ℕ
a : Lex (ℕ × ℕ)
h₁ : a ≤ (i + 1, 0)
⊢ lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
cases h₁
State after:
case left
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁✝ b₁✝ : ℕ
h✝ : a₁✝ < i + 1
⊢ lindenbaumSequence t Δ (a₁✝, b₁✝) ⊆ lindenbaumSequence t Δ (i + 1, 0)

case right
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i b₁✝ : ℕ
h✝ : b₁✝ ≤ 0
⊢ lindenbaumSequence t Δ (i + 1, b₁✝) ⊆ lindenbaumSequence t Δ (i + 1, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
case left a₁ b₁ h₂ => 
  have l₁ : a₁ < i ∨ a₁ = i := Nat.lt_or_eq_of_le $ Nat.lt_succ.mp h₂
  have l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁ := by 
    cases l₁
    case inl h₂ => exact Or.inl h₂
    case inr h₂ => exact Or.inr ⟨h₂, le_refl b₁⟩
  have l₃ := (Prod.Lex.le_iff (a₁, b₁) (i,b₁)).mpr l₂
  have l₄ := @lindenbaumSequenceMonotone' t Δ (i,b₁) (a₁, b₁) l₃
  apply le_trans l₄
  intros f h₂
  exact ⟨b₁,h₂⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i b₁ : ℕ
h₂ : b₁ ≤ 0
⊢ lindenbaumSequence t Δ (i + 1, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
case right b₁ h₂ =>
  rw [Nat.le_zero_eq b₁] at h₂
  rw [h₂]
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
have l₁ : a₁ < i ∨ a₁ = i := Nat.lt_or_eq_of_le $ Nat.lt_succ.mp h₂
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
have l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁ := by 
  cases l₁
  case inl h₂ => exact Or.inl h₂
  case inr h₂ => exact Or.inr ⟨h₂, le_refl b₁⟩
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
have l₃ := (Prod.Lex.le_iff (a₁, b₁) (i,b₁)).mpr l₂
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
l₃ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, b₁)
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
l₃ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, b₁)
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
have l₄ := @lindenbaumSequenceMonotone' t Δ (i,b₁) (a₁, b₁) l₃
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
l₃ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, b₁)
l₄ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, b₁)
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
l₃ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, b₁)
l₄ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, b₁)
⊢ lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
apply le_trans l₄
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
l₃ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, b₁)
l₄ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, b₁)
⊢ lindenbaumSequence t Δ (i, b₁) ≤ lindenbaumSequence t Δ (i + 1, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
l₃ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, b₁)
l₄ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, b₁)
⊢ lindenbaumSequence t Δ (i, b₁) ≤ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
intros f h₂
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂✝ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
l₃ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, b₁)
l₄ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, b₁)
f : Form
h₂ : f ∈ lindenbaumSequence t Δ (i, b₁)
⊢ f ∈ lindenbaumSequence t Δ (i + 1, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂✝ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
l₂ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
l₃ : ↑toLex (a₁, b₁) ≤ ↑toLex (i, b₁)
l₄ : lindenbaumSequence t Δ (a₁, b₁) ⊆ lindenbaumSequence t Δ (i, b₁)
f : Form
h₂ : f ∈ lindenbaumSequence t Δ (i, b₁)
⊢ f ∈ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
exact ⟨b₁,h₂⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
l₁ : a₁ < i ∨ a₁ = i
⊢ a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
Tactic:
cases l₁
State after:
case inl
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
h✝ : a₁ < i
⊢ a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁

case inr
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂ : a₁ < i + 1
h✝ : a₁ = i
⊢ a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂✝ : a₁ < i + 1
h₂ : a₁ < i
⊢ a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
Tactic:
case inl h₂ => exact Or.inl h₂
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂✝ : a₁ < i + 1
h₂ : a₁ = i
⊢ a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
Tactic:
case inr h₂ => exact Or.inr ⟨h₂, le_refl b₁⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂✝ : a₁ < i + 1
h₂ : a₁ < i
⊢ a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
Tactic:
exact Or.inl h₂
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i a₁ b₁ : ℕ
h₂✝ : a₁ < i + 1
h₂ : a₁ = i
⊢ a₁ < i ∨ a₁ = i ∧ b₁ ≤ b₁
Tactic:
exact Or.inr ⟨h₂, le_refl b₁⟩
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i b₁ : ℕ
h₂ : b₁ ≤ 0
⊢ lindenbaumSequence t Δ (i + 1, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
rw [Nat.le_zero_eq b₁] at h₂
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i b₁ : ℕ
h₂ : b₁ = 0
⊢ lindenbaumSequence t Δ (i + 1, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i b₁ : ℕ
h₂ : b₁ = 0
⊢ lindenbaumSequence t Δ (i + 1, b₁) ⊆ lindenbaumSequence t Δ (i + 1, 0)
Tactic:
rw [h₂]
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ (i, j + 1) → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
have lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1) := by
  intros f h₃
  unfold lindenbaumSequence
  split
  case h_1 _ heq | h_2 _ heq => injection heq; contradiction
  case h_3 i' j' heq =>
    injection heq with heq₁ heq₂
    injection heq₂ with heq₂
    have heq₃ : j = j' := heq₂
    rw [←heq₁, ←heq₃]
    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
    intros prev l r
    split
    case inl =>
      split
      case inl | inr => apply Or.inl h₃
    case inr => exact h₃
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ (i, j + 1) → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i, j + 1)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ (i, j + 1) → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
intros a h₁
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a : Lex (ℕ × ℕ)
h₁ : a ≤ (i, j + 1)
⊢ lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i, j + 1)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
lem : lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
a : Lex (ℕ × ℕ)
h₁ : a ≤ (i, j + 1)
⊢ lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ (i, j + 1)
Tactic:
cases h₁
State after:
case left
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)

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

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:
case left a₁ b₁ h₂ =>
    have l₁ : a₁ < i ∨ a₁ = i ∧ b₁ ≤ j := Or.inl h₂
    have l₂ := (Prod.Lex.le_iff (a₁, b₁) (i,j)).mpr l₁
    have l₃ := @lindenbaumSequenceMonotone' t Δ (i,j) (a₁, b₁)  l₂
    apply le_trans l₃
    exact lem
State after:
no goals

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:
case right b₁ h₂ =>
  cases h₂
  case refl => intros _ h₁; assumption
  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
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
⊢ lindenbaumSequence t Δ (i, j) ≤ lindenbaumSequence t Δ (i, j + 1)
Tactic:
intros f h₃
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
⊢ f ∈ lindenbaumSequence t Δ (i, j + 1)

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
⊢ f ∈ lindenbaumSequence t Δ (i, j + 1)
Tactic:
unfold lindenbaumSequence
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
⊢ f ∈
    match (i, j + 1) with
    | (0, 0) => ↑t
    | (Nat.succ i, 0) => { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
    | (i, Nat.succ j) =>
      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

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
⊢ f ∈
    match (i, j + 1) with
    | (0, 0) => ↑t
    | (Nat.succ i, 0) => { f | ∃ j, f ∈ lindenbaumSequence t Δ (i, j) }
    | (i, Nat.succ j) =>
      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:
split
State after:
case h_1
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
heq✝ : (i, j + 1) = (0, 0)
⊢ f ∈ ↑t

case h_2
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i✝ : ℕ
heq✝ : (i, j + 1) = (Nat.succ i✝, 0)
⊢ f ∈ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i✝, j) }

case h_3
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i✝ j✝ : ℕ
heq✝ : (i, j + 1) = (i✝, Nat.succ 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

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i✝ : ℕ
heq : (i, j + 1) = (Nat.succ i✝, 0)
⊢ f ∈ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i✝, j) }
Tactic:
case h_1 _ heq | h_2 _ heq => injection heq; contradiction
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq : (i, j + 1) = (i', Nat.succ 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:
case h_3 i' j' heq =>
  injection heq with heq₁ heq₂
  injection heq₂ with heq₂
  have heq₃ : j = j' := heq₂
  rw [←heq₁, ←heq₃]
  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
  intros prev l r
  split
  case inl =>
    split
    case inl | inr => apply Or.inl h₃
  case inr => exact h₃
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i✝ : ℕ
heq : (i, j + 1) = (Nat.succ i✝, 0)
⊢ f ∈ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i✝, j) }
Tactic:
injection heq
State after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i✝ : ℕ
fst_eq✝ : i = Nat.succ i✝
snd_eq✝ : j + 1 = 0
⊢ f ∈ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i✝, j) }

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i✝ : ℕ
fst_eq✝ : i = Nat.succ i✝
snd_eq✝ : j + 1 = 0
⊢ f ∈ { f | ∃ j, f ∈ lindenbaumSequence t Δ (i✝, j) }
Tactic:
contradiction
State after:
no goals

State before:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
i j : ℕ
f : Form
h₃ : f ∈ lindenbaumSequence t Δ (i, j)
x✝ : Lex (ℕ × ℕ)
i' j' : ℕ
heq : (i, j + 1) = (i', Nat.succ 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:
injection heq with heq₁ heq₂
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₂ : j + 1 = Nat.succ 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

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₂ : j + 1 = Nat.succ 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:
injection heq₂ with heq₂
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'
⊢ 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

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'
⊢ 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:
have heq₃ : j = j' := heq₂
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'
⊢ 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

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:
rw [←heq₁, ←heq₃]
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'
⊢ 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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