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

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ lindenbaumExtension t Δ ∩ Δ = ∅
Tactic:
unfold lindenbaumExtension
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ { f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ = ∅

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ { f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ = ∅
Tactic:
apply Set.not_nonempty_iff_eq_empty.mp
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ ¬Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ ¬Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
Tactic:
intros h₃
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
h₃ : Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
h₃ : Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
⊢ False
Tactic:
have ⟨f, ⟨ij, h₄⟩, h₅⟩ := h₃
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
h₃ : Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
f : Form
ij : ℕ × ℕ
h₄ : f ∈ lindenbaumSequence t Δ ij
h₅ : f ∈ Δ
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
h₃ : Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
f : Form
ij : ℕ × ℕ
h₄ : f ∈ lindenbaumSequence t Δ ij
h₅ : f ∈ Δ
⊢ False
Tactic:
have l₁ := lindenbaumAvoids h₁ h₂ ij
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
h₃ : Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
f : Form
ij : ℕ × ℕ
h₄ : f ∈ lindenbaumSequence t Δ ij
h₅ : f ∈ Δ
l₁ : ▲lindenbaumSequence t Δ ij ∩ Δ = ∅
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
h₃ : Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
f : Form
ij : ℕ × ℕ
h₄ : f ∈ lindenbaumSequence t Δ ij
h₅ : f ∈ Δ
l₁ : ▲lindenbaumSequence t Δ ij ∩ Δ = ∅
⊢ False
Tactic:
have l₂ : f ∈ ▲lindenbaumSequence t Δ ij := ⟨BProof.ax h₄⟩
State after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
h₃ : Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
f : Form
ij : ℕ × ℕ
h₄ : f ∈ lindenbaumSequence t Δ ij
h₅ : f ∈ Δ
l₁ : ▲lindenbaumSequence t Δ ij ∩ Δ = ∅
l₂ : f ∈ ▲lindenbaumSequence t Δ ij
⊢ False

State before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
h₃ : Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
f : Form
ij : ℕ × ℕ
h₄ : f ∈ lindenbaumSequence t Δ ij
h₅ : f ∈ Δ
l₁ : ▲lindenbaumSequence t Δ ij ∩ Δ = ∅
l₂ : f ∈ ▲lindenbaumSequence t Δ ij
⊢ False
Tactic:
exact Set.not_nonempty_iff_eq_empty.mpr l₁ $ ⟨f, l₂, h₅⟩
State after:
no goals