internlm/Lean-Github huggingface dataset:
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
⊢ ↑(fin₁ ∪ fin₂) ⊆ Γ
Tactic:
intros f h₃
Proof state after:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₃ : f ∈ ↑(fin₁ ∪ fin₂)
⊢ f ∈ Γ
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₃ : f ∈ ↑(fin₁ ∪ fin₂)
⊢ f ∈ Γ
Tactic:
rw [Finset.coe_union] at h₃
Proof state after:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₃ : f ∈ ↑fin₁ ∪ ↑fin₂
⊢ f ∈ Γ
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₃ : f ∈ ↑fin₁ ∪ ↑fin₂
⊢ f ∈ Γ
Tactic:
cases h₃
Proof state after:
case inl
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h✝ : f ∈ ↑fin₁
⊢ f ∈ Γ

case inr
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h✝ : f ∈ ↑fin₂
⊢ f ∈ Γ
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₄ : f ∈ ↑fin₁
⊢ f ∈ Γ
Tactic:
case inl h₄ => exact h₁ h₄
Proof state after:
no goals
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₄ : f ∈ ↑fin₂
⊢ f ∈ Γ
Tactic:
case inr h₄ => exact h₂ h₄
Proof state after:
no goals
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₄ : f ∈ ↑fin₁
⊢ f ∈ Γ
Tactic:
exact h₁ h₄
Proof state after:
no goals
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₄ : f ∈ ↑fin₂
⊢ f ∈ Γ
Tactic:
exact h₂ h₄
Proof state after:
no goals
Theorem: BProof.listCompression
Proof state before:
l : List Form
f g : Form
⊢ BProof { h | h = f ∨ h ∈ l } g → BProof {Form.conjoinList f l} g
Tactic:
intros prf₁
Proof state after:
l : List Form
f g : Form
prf₁ : BProof { h | h = f ∨ h ∈ l } g
⊢ BProof {Form.conjoinList f l} g
Theorem: BProof.listCompression
Proof state before:
l : List Form
f g : Form
prf₁ : BProof { h | h = f ∨ h ∈ l } g
⊢ BProof {Form.conjoinList f l} g
Tactic:
induction prf₁
Proof state after:
case ax
l : List Form
f g p✝ : Form
h✝ : p✝ ∈ { h | h = f ∨ h ∈ l }
⊢ BProof {Form.conjoinList f l} p✝

case mp
l : List Form
f g p✝ q✝ : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : BProof {Form.conjoinList f l} p✝
⊢ BProof {Form.conjoinList f l} q✝

case adj
l : List Form
f g p✝ q✝ : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p✝
h₂✝ : BProof { h | h = f ∨ h ∈ l } q✝
h₁_ih✝ : BProof {Form.conjoinList f l} p✝
h₂_ih✝ : BProof {Form.conjoinList f l} q✝
⊢ BProof {Form.conjoinList f l} (p✝&q✝)
Theorem: BProof.listCompression
Proof state before:
l : List Form
f g p : Form
h₁ : p ∈ { h | h = f ∨ h ∈ l }
⊢ BProof {Form.conjoinList f l} p
Tactic:
case ax p h₁ => exact BProof.proveFromList $ List.mem_cons.mpr h₁
Proof state after:
no goals
Theorem: BProof.listCompression
Proof state before:
l : List Form
f g p q : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p
prf₂ : BTheorem (p⊃q)
ih : BProof {Form.conjoinList f l} p
⊢ BProof {Form.conjoinList f l} q
Tactic:
case mp p q _ prf₂ ih => exact BProof.mp ih prf₂
Proof state after:
no goals
Theorem: BProof.listCompression
Proof state before:
l : List Form
f g p q : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p
h₂✝ : BProof { h | h = f ∨ h ∈ l } q
prf₁ : BProof {Form.conjoinList f l} p
prf₂ : BProof {Form.conjoinList f l} q
⊢ BProof {Form.conjoinList f l} (p&q)
Tactic:
case adj p q _ _ prf₁ prf₂  => exact BProof.adj prf₁ prf₂
Proof state after:
no goals
Theorem: BProof.listCompression
Proof state before:
l : List Form
f g p : Form
h₁ : p ∈ { h | h = f ∨ h ∈ l }
⊢ BProof {Form.conjoinList f l} p
Tactic:
exact BProof.proveFromList $ List.mem_cons.mpr h₁
Proof state after:
no goals
Theorem: BProof.listCompression
Proof state before:
l : List Form
f g p q : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p
prf₂ : BTheorem (p⊃q)
ih : BProof {Form.conjoinList f l} p
⊢ BProof {Form.conjoinList f l} q
Tactic:
exact BProof.mp ih prf₂
Proof state after:
no goals
Theorem: BProof.listCompression
Proof state before:
l : List Form
f g p q : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p
h₂✝ : BProof { h | h = f ∨ h ∈ l } q
prf₁ : BProof {Form.conjoinList f l} p
prf₂ : BProof {Form.conjoinList f l} q
⊢ BProof {Form.conjoinList f l} (p&q)
Tactic:
exact BProof.adj prf₁ prf₂
Proof state after:
no goals
Theorem: BProof.sentenceCompactness
Proof 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₁
Proof state after:
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g
Theorem: BProof.sentenceCompactness
Proof 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₁
Proof 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
Theorem: BProof.sentenceCompactness
Proof 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
Proof 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
Theorem: BProof.sentenceCompactness
Proof 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₂
Proof 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
Theorem: BProof.sentenceCompactness
Proof 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₁
Proof 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
Theorem: BProof.sentenceCompactness
Proof 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₂⟩
Proof 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₁ } ⊆ Γ
Theorem: BProof.sentenceCompactness
Proof 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₃
Proof 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 ∈ Γ
Theorem: BProof.sentenceCompactness
Proof 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₃
Proof 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 ∈ Γ
Theorem: BProof.sentenceCompactness
Proof 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
Proof 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 ∈ Γ
Theorem: BProof.sentenceCompactness
Proof 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₆
Proof 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 ∈ Γ
Theorem: BProof.sentenceCompactness
Proof 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₅
Proof state after:
no goals
Theorem: BProof.sentenceCompactness
Proof 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₂
Proof 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₁ }
Theorem: BProof.sentenceCompactness
Proof 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
Proof 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₁ }
Theorem: BProof.sentenceCompactness
Proof 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
Proof state after:
no goals
Theorem: BProof.sentenceCompactness
Proof 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₂
Proof state after:
no goals
Theorem: BProof.sentenceCompactness
Proof 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₃]
Proof 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₁ }
Theorem: BProof.sentenceCompactness
Proof 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
Proof state after:
no goals
Theorem: BProof.sentenceCompactness
Proof 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₂⟩
Proof 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₁ }
Theorem: BProof.sentenceCompactness
Proof 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₂
Proof state after:
no goals
Theorem: BProof.sentenceCompactness
Proof 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
Proof 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
Theorem: BProof.sentenceCompactness
Proof 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₂⟩
Proof state after:
no goals
Theorem: finiteExhaustion
Proof state before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
⊢ Monotone fam → ↑fin ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fin ⊆ fam n
Tactic:
intros h₁
Proof state after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑fin ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fin ⊆ fam n
Theorem: finiteExhaustion
Proof state before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑fin ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑fin ⊆ fam n
Tactic:
apply @Finset.induction_on α (λfs => ↑fs ⊆ {x : α | ∃n : β, x ∈ fam n } → ∃n : β, ↑fs ⊆ fam n) instDec fin
Proof state after:
case empty
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑∅ ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑∅ ⊆ fam n

case insert
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (↑s ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑s ⊆ fam n) →
        ↑(insert a s) ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑(insert a s) ⊆ fam n
Theorem: finiteExhaustion
Proof state before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑∅ ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑∅ ⊆ fam n
Tactic:
case empty =>
  intros _
  refine ⟨default,?_⟩
  intros h₂ h₃
  contradiction
Proof state after:
no goals
Theorem: finiteExhaustion
Proof state before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (↑s ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑s ⊆ fam n) →
        ↑(insert a s) ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑(insert a s) ⊆ fam n
Tactic:
case insert => 
  intros x fs _ h₃ h₄
  have l₁ : x ∈ {x : α | ∃n : β, x ∈ fam n } := h₄ $ Finset.mem_insert_self x fs
  have ⟨n, l₂⟩ := l₁
  have l₃ : ↑fs ⊆ {x : α | ∃n : β, x ∈ fam n } := by
    intros y h₅
    exact h₄ $ Finset.mem_insert_of_mem (Finset.mem_coe.mp h₅)
  have ⟨m, l₄⟩ := h₃ l₃
  cases le_total n m
  case inl leqthan => 
    have l₅ := (h₁ leqthan) l₂
    refine ⟨m,?_⟩
    intros y h₄
    cases Finset.mem_insert.mp h₄
    case inl h₅ => rw [h₅]; assumption
    case inr h₅ => exact l₄ h₅
  case inr geqthan =>
    have l₅ := le_trans l₄ (h₁ geqthan) 
    refine ⟨n,?_⟩
    intros y h₄
    cases Finset.mem_insert.mp h₄
    case inl h₅ => rw [h₅]; assumption
    case inr h₅ => exact l₅ h₅
Proof state after:
no goals
Theorem: finiteExhaustion
Proof state before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
⊢ ↑∅ ⊆ { x | ∃ n, x ∈ fam n } → ∃ n, ↑∅ ⊆ fam n
Tactic:
intros _
Proof state after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
⊢ ∃ n, ↑∅ ⊆ fam n
Theorem: finiteExhaustion
Proof state before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
⊢ ∃ n, ↑∅ ⊆ fam n
Tactic:
refine ⟨default,?_⟩
Proof state after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
⊢ ↑∅ ⊆ fam default
Theorem: finiteExhaustion
Proof state before:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
⊢ ↑∅ ⊆ fam default
Tactic:
intros h₂ h₃
Proof state after:
α : Type u_1
β : Type u_2
instDec : DecidableEq α
inst✝¹ : LinearOrder β
inst✝ : Inhabited β
fam : β → Set α
fin : Finset α
h₁ : Monotone fam
a✝ : ↑∅ ⊆ { x | ∃ n, x ∈ fam n }
h₂ : α
h₃ : h₂ ∈ ↑∅
⊢ h₂ ∈ fam default