Theorem: BProof.sentenceCompactness (Fine/SystemB/Hilbert.lean)

State before:
Γ : Ctx
f g : Form
⊢ BProof (insert f Γ) g → (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g
Tactic:
intros h₁
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g
Tactic:
have ⟨s₁,h₂,prf₁⟩ := BProof.compactness h₁
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g
Tactic:
let lst₁ := (Finset.erase s₁ f).toList
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g
Tactic:
have l₁ : ↑s₁ ⊆ {h : Form | h = f ∨ h ∈ lst₁} := by
  intros k h₂
  cases decEq f k
  case isTrue h₃ => rw [h₃]; exact Or.inl rfl
  case isFalse h₃ => 
    have l₂ : k ∈ lst₁ := by
      apply Finset.mem_toList.mpr
      exact Finset.mem_erase.mpr ⟨h₃ ∘ Eq.symm, h₂⟩
    exact Or.inr l₂
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g
Tactic:
have prf₂ := BProof.listCompression $  BProof.monotone l₁ prf₁
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g
Tactic:
refine ⟨lst₁,?_,prf₂⟩
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
⊢ { x | x ∈ lst₁ } ⊆ Γ

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
⊢ { x | x ∈ lst₁ } ⊆ Γ
Tactic:
intros k h₃
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
k : Form
h₃ : k ∈ { x | x ∈ lst₁ }
⊢ k ∈ Γ

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
k : Form
h₃ : k ∈ { x | x ∈ lst₁ }
⊢ k ∈ Γ
Tactic:
have : k ∈ Finset.erase s₁ f := Finset.mem_toList.mp h₃
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
k : Form
h₃ : k ∈ { x | x ∈ lst₁ }
this : k ∈ Finset.erase s₁ f
⊢ k ∈ Γ

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
k : Form
h₃ : k ∈ { x | x ∈ lst₁ }
this : k ∈ Finset.erase s₁ f
⊢ k ∈ Γ
Tactic:
have ⟨l₅,l₆⟩: k ≠ f ∧ k ∈ s₁ := Finset.mem_erase.mp this
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
k : Form
h₃ : k ∈ { x | x ∈ lst₁ }
this : k ∈ Finset.erase s₁ f
l₅ : k ≠ f
l₆ : k ∈ s₁
⊢ k ∈ Γ

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
k : Form
h₃ : k ∈ { x | x ∈ lst₁ }
this : k ∈ Finset.erase s₁ f
l₅ : k ≠ f
l₆ : k ∈ s₁
⊢ k ∈ Γ
Tactic:
have : k ∈ insert f Γ := h₂ $ Finset.mem_coe.mpr l₆
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
k : Form
h₃ : k ∈ { x | x ∈ lst₁ }
this✝ : k ∈ Finset.erase s₁ f
l₅ : k ≠ f
l₆ : k ∈ s₁
this : k ∈ insert f Γ
⊢ k ∈ Γ

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
prf₂ : BProof {Form.conjoinList f lst₁} g
k : Form
h₃ : k ∈ { x | x ∈ lst₁ }
this✝ : k ∈ Finset.erase s₁ f
l₅ : k ≠ f
l₆ : k ∈ s₁
this : k ∈ insert f Γ
⊢ k ∈ Γ
Tactic:
exact Set.mem_of_mem_insert_of_ne this l₅
State after:
no goals

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
⊢ ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
Tactic:
intros k h₂
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
⊢ k ∈ { h | h = f ∨ h ∈ lst₁ }

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
⊢ k ∈ { h | h = f ∨ h ∈ lst₁ }
Tactic:
cases decEq f k
State after:
case isFalse
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h✝ : ¬f = k
⊢ k ∈ { h | h = f ∨ h ∈ lst₁ }

case isTrue
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h✝ : f = k
⊢ k ∈ { h | h = f ∨ h ∈ lst₁ }

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : f = k
⊢ k ∈ { h | h = f ∨ h ∈ lst₁ }
Tactic:
case isTrue h₃ => rw [h₃]; exact Or.inl rfl
State after:
no goals

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : ¬f = k
⊢ k ∈ { h | h = f ∨ h ∈ lst₁ }
Tactic:
case isFalse h₃ => 
  have l₂ : k ∈ lst₁ := by
    apply Finset.mem_toList.mpr
    exact Finset.mem_erase.mpr ⟨h₃ ∘ Eq.symm, h₂⟩
  exact Or.inr l₂
State after:
no goals

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : f = k
⊢ k ∈ { h | h = f ∨ h ∈ lst₁ }
Tactic:
rw [h₃]
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : f = k
⊢ k ∈ { h | h = k ∨ h ∈ lst₁ }

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : f = k
⊢ k ∈ { h | h = k ∨ h ∈ lst₁ }
Tactic:
exact Or.inl rfl
State after:
no goals

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : ¬f = k
⊢ k ∈ { h | h = f ∨ h ∈ lst₁ }
Tactic:
have l₂ : k ∈ lst₁ := by
  apply Finset.mem_toList.mpr
  exact Finset.mem_erase.mpr ⟨h₃ ∘ Eq.symm, h₂⟩
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : ¬f = k
l₂ : k ∈ lst₁
⊢ k ∈ { h | h = f ∨ h ∈ lst₁ }

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : ¬f = k
l₂ : k ∈ lst₁
⊢ k ∈ { h | h = f ∨ h ∈ lst₁ }
Tactic:
exact Or.inr l₂
State after:
no goals

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : ¬f = k
⊢ k ∈ lst₁
Tactic:
apply Finset.mem_toList.mpr
State after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : ¬f = k
⊢ k ∈ Finset.erase s₁ f

State before:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂✝ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
k : Form
h₂ : k ∈ ↑s₁
h₃ : ¬f = k
⊢ k ∈ Finset.erase s₁ f
Tactic:
exact Finset.mem_erase.mpr ⟨h₃ ∘ Eq.symm, h₂⟩
State after:
no goals