internlm/Lean-Github huggingface dataset:
Theorem: lindenbaumAvoids
Proof state before:
case cons.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head : Form
tail : List Form
l₆ : { x | x ∈ head :: tail } ⊆ lindenbaumSequence t Δ (i, j + 0)
head' : Form
tail' : List Form
l₇ : { x | x ∈ head' :: tail' } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head' :: tail')¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
prf₆ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
prf₇ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head' tail')
this :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j +
              0)).fst&Form.conjoinList head'
          tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head' tail')
prf₈ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j + 0)).fst&Form.conjoinList head' tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
⊢ False
Tactic:
have := BProof.mp (BProof.adj prf₈ prf₆) BTheorem.distRight
Proof state after:
case cons.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head : Form
tail : List Form
l₆ : { x | x ∈ head :: tail } ⊆ lindenbaumSequence t Δ (i, j + 0)
head' : Form
tail' : List Form
l₇ : { x | x ∈ head' :: tail' } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head' :: tail')¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
prf₆ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
prf₇ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head' tail')
this✝ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j +
              0)).fst&Form.conjoinList head'
          tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head' tail')
prf₈ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j + 0)).fst&Form.conjoinList head' tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
this :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((((Denumerable.ofNat (Form × Form)
              (j +
                0)).fst&Form.conjoinList head'
            tail')&Form.conjoinList head tail)¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
⊢ False
Theorem: lindenbaumAvoids
Proof state before:
case cons.cons
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
i j : ℕ
w₁ : Form
l₃ : ▲lindenbaumSequence t Δ (i, j) ∩ Δ = ∅
w₂ : Form
l₅ : w₁¦w₂ ∈ Δ
prf₅ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((Denumerable.ofNat (Form × Form) (j + 0)).fst¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
head : Form
tail : List Form
l₆ : { x | x ∈ head :: tail } ⊆ lindenbaumSequence t Δ (i, j + 0)
head' : Form
tail' : List Form
l₇ : { x | x ∈ head' :: tail' } ⊆ lindenbaumSequence t Δ (i, j + 0)
thm₃ :
  BTheorem
    (Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).fst
          (head' :: tail')¦Form.conjoinList (Denumerable.ofNat (Form × Form) (j + 0)).snd (head :: tail)⊃w₁¦w₂)
prf₆ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head tail)
prf₇ : BProof (lindenbaumSequence t Δ (i, j + 0)) (Form.conjoinList head' tail')
this✝¹ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j +
              0)).fst&Form.conjoinList head'
          tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head' tail')
prf₈ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j + 0)).fst&Form.conjoinList head' tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd)
this✝ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    ((((Denumerable.ofNat (Form × Form)
              (j +
                0)).fst&Form.conjoinList head'
            tail')&Form.conjoinList head tail)¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
prf₉ :
  BProof (lindenbaumSequence t Δ (i, j + 0))
    (((Denumerable.ofNat (Form × Form)
            (j +
              0)).fst&Form.conjoinList head'
          tail')¦(Denumerable.ofNat (Form × Form) (j + 0)).snd&Form.conjoinList head tail)
this : w₁¦w₂ ∈ ▲lindenbaumSequence t Δ (i, j) ∩ Δ
⊢ False
Tactic:
exact (Set.not_nonempty_iff_eq_empty.mpr l₃) ⟨w₁¦w₂, this⟩
Proof state after:
no goals
Theorem: lindenbaumTheorem
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ lindenbaumExtension t Δ ∩ Δ = ∅
Tactic:
unfold lindenbaumExtension
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ { f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ = ∅
Theorem: lindenbaumTheorem
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ { f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ = ∅
Tactic:
apply Set.not_nonempty_iff_eq_empty.mp
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ ¬Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
Theorem: lindenbaumTheorem
Proof state before:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
⊢ ¬Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
Tactic:
intros h₃
Proof state after:
t : Th
Δ : Ctx
h₁ : ↑t ∩ Δ = ∅
h₂ : isDisjunctionClosed Δ
h₃ : Set.Nonempty ({ f | ∃ ij, f ∈ lindenbaumSequence t Δ ij } ∩ Δ)
⊢ False
Theorem: lindenbaumTheorem
Proof 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₃
Proof 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
Theorem: lindenbaumTheorem
Proof 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
Proof 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
Theorem: lindenbaumTheorem
Proof 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₄⟩
Proof 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
Theorem: lindenbaumTheorem
Proof 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₅⟩
Proof state after:
no goals
Theorem: Form.toConsExp_injective
Proof state before:
⊢ Function.Injective toConsExp
Tactic:
intros f1 f2
Proof state after:
f1 f2 : Form
⊢ toConsExp f1 = toConsExp f2 → f1 = f2
Theorem: Form.toConsExp_injective
Proof state before:
f1 f2 : Form
⊢ toConsExp f1 = toConsExp f2 → f1 = f2
Tactic:
induction f1 generalizing f2 <;> cases f2 <;> simp! <;> aesop
Proof state after:
no goals
Theorem: Form.nat_injection
Proof state before:
⊢ Function.Injective atom
Tactic:
unfold Function.Injective
Proof state after:
⊢ ∀ ⦃a₁ a₂ : ℕ⦄, #a₁ = #a₂ → a₁ = a₂
Theorem: Form.nat_injection
Proof state before:
⊢ ∀ ⦃a₁ a₂ : ℕ⦄, #a₁ = #a₂ → a₁ = a₂
Tactic:
intros n m h₁
Proof state after:
n m : ℕ
h₁ : #n = #m
⊢ n = m
Theorem: Form.nat_injection
Proof state before:
n m : ℕ
h₁ : #n = #m
⊢ n = m
Tactic:
injection h₁
Proof state after:
no goals
Theorem: toForm_toConsExp_eq
Proof state before:
f : Form
⊢ ConsExp.toForm (Form.toConsExp f) = some f
Tactic:
induction f <;> simp! [*]
Proof state after:
no goals
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f : Form
⊢ BProof Γ f → (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) f
Tactic:
intros prf₁
Proof state after:
Γ : Ctx
f : Form
prf₁ : BProof Γ f
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) f
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f : Form
prf₁ : BProof Γ f
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) f
Tactic:
induction prf₁
Proof state after:
case ax
Γ : Ctx
f p✝ : Form
h✝ : p✝ ∈ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) p✝

case mp
Γ : Ctx
f p✝ q✝ : Form
h₁✝ : BProof Γ p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) p✝
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) q✝

case adj
Γ : Ctx
f p✝ q✝ : Form
h₁✝ : BProof Γ p✝
h₂✝ : BProof Γ q✝
h₁_ih✝ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) p✝
h₂_ih✝ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) q✝
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (p✝&q✝)
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
case ax g h₁ => 
  let Gsing : Finset Form := {g} 
  have l₁ : g ∈ {g} := Finset.mem_singleton.mpr rfl
  have l₂ : Gsing = ({g} : Ctx) := Finset.coe_singleton g
  have l₃ : ↑Gsing ⊆ Γ := by
    intros g' h₂
    rw [l₂] at h₂
    rw [h₂]
    assumption
  have prf₂ : BProof ↑{g} g := by
    rw [←l₂]
    apply ax l₁
  rw [←l₂] at prf₂
  exact ⟨Gsing, l₃, prf₂⟩
Proof state after:
no goals
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂ : BTheorem (P⊃Q)
ih : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
Tactic:
case mp P Q _ h₂ ih => 
  have ⟨fin, h₁, prf⟩ := ih
  exact ⟨fin, h₁, mp prf 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
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
case adj P Q _ _ ih₁ ih₂ => 
  have ⟨fin₁, h₁, prf₁⟩ := ih₁
  have ⟨fin₂, h₂, prf₂⟩ := ih₂
  have prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P := BProof.monotone (Set.subset_union_left ↑fin₁ ↑fin₂) prf₁
  have prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q := BProof.monotone (Set.subset_union_right ↑fin₁ ↑fin₂) prf₂
  have prf₅ := adj prf₃ prf₄
  have l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ := by
    intros f h₃
    rw [Finset.coe_union] at h₃
    cases h₃
    case inl h₄ => exact h₁ h₄
    case inr h₄ => exact h₂ h₄
  rw [←Finset.coe_union] at prf₅
  exact ⟨↑(fin₁ ∪ fin₂), l₁, prf₅⟩
Proof state after:
no goals
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
let Gsing : Finset Form := {g}
Proof state after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
have l₁ : g ∈ {g} := Finset.mem_singleton.mpr rfl
Proof state after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
have l₂ : Gsing = ({g} : Ctx) := Finset.coe_singleton g
Proof state after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
have l₃ : ↑Gsing ⊆ Γ := by
  intros g' h₂
  rw [l₂] at h₂
  rw [h₂]
  assumption
Proof state after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
have prf₂ : BProof ↑{g} g := by
  rw [←l₂]
  apply ax l₁
Proof state after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
prf₂ : BProof {g} g
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
prf₂ : BProof {g} g
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
rw [←l₂] at prf₂
Proof state after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
prf₂ : BProof (↑Gsing) g
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
prf₂ : BProof (↑Gsing) g
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
exact ⟨Gsing, l₃, prf₂⟩
Proof state after:
no goals
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
⊢ ↑Gsing ⊆ Γ
Tactic:
intros g' h₂
Proof state after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ ↑Gsing
⊢ g' ∈ Γ
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ ↑Gsing
⊢ g' ∈ Γ
Tactic:
rw [l₂] at h₂
Proof state after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ {g}
⊢ g' ∈ Γ
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ {g}
⊢ g' ∈ Γ
Tactic:
rw [h₂]
Proof state after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ {g}
⊢ g ∈ Γ
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ {g}
⊢ g ∈ Γ
Tactic:
assumption
Proof state after:
no goals
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
⊢ BProof {g} g
Tactic:
rw [←l₂]
Proof state after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
⊢ BProof (↑Gsing) g
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
⊢ BProof (↑Gsing) g
Tactic:
apply ax l₁
Proof state after:
no goals
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂ : BTheorem (P⊃Q)
ih : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
Tactic:
have ⟨fin, h₁, prf⟩ := ih
Proof state after:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂ : BTheorem (P⊃Q)
ih : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
fin : Finset Form
h₁ : ↑fin ⊆ Γ
prf : BProof (↑fin) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
Theorem: BProof.compactness
Proof state before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂ : BTheorem (P⊃Q)
ih : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
fin : Finset Form
h₁ : ↑fin ⊆ Γ
prf : BProof (↑fin) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
Tactic:
exact ⟨fin, h₁, mp prf 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
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have ⟨fin₁, h₁, prf₁⟩ := ih₁
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
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
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
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have ⟨fin₂, h₂, prf₂⟩ := ih₂
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
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
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
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P := BProof.monotone (Set.subset_union_left ↑fin₁ ↑fin₂) prf₁
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
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
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
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q := BProof.monotone (Set.subset_union_right ↑fin₁ ↑fin₂) prf₂
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
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
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
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have prf₅ := adj prf₃ prf₄
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)
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
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)
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ := by
  intros f h₃
  rw [Finset.coe_union] at h₃
  cases h₃
  case inl h₄ => exact h₁ h₄
  case inr h₄ => exact h₂ 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)
l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
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)
l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
rw [←Finset.coe_union] at prf₅
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)
prf₅ : BProof (↑(fin₁ ∪ fin₂)) (P&Q)
l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
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)
prf₅ : BProof (↑(fin₁ ∪ fin₂)) (P&Q)
l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
exact ⟨↑(fin₁ ∪ fin₂), l₁, prf₅⟩
Proof state after:
no goals