Theorem: lindenbaumAvoids
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
h₃ : Set.Nonempty (▲lindenbaumSequence t Δ (i, j + 1) ∩ Δ)
w₁ : Form
l₂ : w₁ ∈ Δ
x : Lex (ℕ × ℕ)
n m : ℕ
heq : (i, j + 1) = (n, Nat.succ m)
l₁ :
  w₁ ∈
    ▲let prev := lindenbaumSequence t Δ (n, m);
      let l := (Denumerable.ofNat (Form × Form) m).fst;
      let r := (Denumerable.ofNat (Form × Form) m).snd;
      if l¦r ∈ ▲prev then if ▲(prev ∪ {l}) ∩ Δ = ∅ then prev ∪ {l} else prev ∪ {r} else prev
⊢ False
Tactic:
case h_3 x n m heq =>
  have l₃ := lindenbaumAvoids h₁ h₂ ⟨i,j⟩
  injection heq with heq₁ heq₂
  injection heq₂ with heq₂
  rw [←heq₁,←heq₂] at l₁
  clear n m x heq₁ heq₂ h₃
  dsimp at l₁ j
  split at l₁
  case inr h₄ => exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁, l₁, l₂⟩
  case inl h₄ =>
    split at l₁
    case inl h₅ => exact (Set.not_nonempty_iff_eq_empty.mpr h₅) ⟨w₁, l₁, l₂⟩
    case inr h₅ =>
      have ⟨prf₁⟩ := l₁
      have ⟨w₂,⟨⟨prf₂⟩,l₄⟩⟩ := Set.nonempty_iff_ne_empty.mpr h₅
      have l₅ : w₁¦w₂ ∈ Δ := h₂ ⟨l₂, l₄⟩
      clear l₁ l₂ l₄ h₅
      have ⟨lst₁,l₆,prf₃⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₁)
      have ⟨lst₂,l₇,prf₄⟩ := BProof.sentenceCompactness (Set.union_singleton ▸ prf₂)
      have thm₁ := BTheorem.transitivity prf₃.toTheorem (BTheorem.orI₁ : BTheorem (w₁ ⊃ w₁ ¦ w₂))
      have thm₂ := BTheorem.transitivity prf₄.toTheorem (BTheorem.orI₂ : BTheorem (w₂ ⊃ w₁ ¦ w₂))
      have thm₃ := BTheorem.mp (BTheorem.adj thm₂ thm₁) BTheorem.orE 
      have ⟨prf₅⟩ := h₄
      clear h₄ thm₁ thm₂ prf₁ prf₂ prf₃ prf₄
      cases lst₁
      all_goals 
        cases lst₂
      case' nil.nil =>
        have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₅ thm₃⟩, l₅⟩
        exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
      case' nil.cons head tail =>
        have := BProof.proveList l₇
        have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
        have := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
        have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
        exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
      case' cons.nil head tail => 
        have := BProof.proveList l₆
        have := BProof.mp (BProof.adj prf₅ this) BTheorem.distRight
        have := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
        have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp this thm₃⟩, l₅⟩
        exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
      case' cons.cons head tail head' tail'=> 
        have prf₆ := BProof.proveList l₆
        have prf₇ := BProof.proveList l₇
        have := BProof.mp (BProof.adj prf₅ prf₇) BTheorem.distRight
        have prf₈ := BProof.mp this (BTheorem.orFunctor BTheorem.taut BTheorem.andE₁)
        have := BProof.mp (BProof.adj prf₈ prf₆) BTheorem.distRight
        have prf₉ := BProof.mp this (BTheorem.orFunctor BTheorem.andE₁ BTheorem.taut)
        have : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ := ⟨⟨BProof.mp prf₉ thm₃⟩, l₅⟩
        exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
Proof state after:
no goals