internlm/Lean-Github huggingface dataset:
Theorem: primeAnalysis
Proof state before:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
l₂ : ↑t ∩ generatedDisjunctions x = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions x)
l₄ : x ∈ generatedDisjunctions x
⊢ False
Tactic:
have l₅ := lindenbaumTheorem l₂ l₃
Proof state after:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
l₂ : ↑t ∩ generatedDisjunctions x = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions x)
l₄ : x ∈ generatedDisjunctions x
l₅ : lindenbaumExtension t (generatedDisjunctions x) ∩ generatedDisjunctions x = ∅
⊢ False
Theorem: primeAnalysis
Proof state before:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
l₂ : ↑t ∩ generatedDisjunctions x = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions x)
l₄ : x ∈ generatedDisjunctions x
l₅ : lindenbaumExtension t (generatedDisjunctions x) ∩ generatedDisjunctions x = ∅
⊢ False
Tactic:
have l₆ := (Set.mem_interₛ.mp h₁) 
  (lindenbaumExtension t (generatedDisjunctions x)) 
  ⟨lindenbaumIsPrime, lindenbaumExtensionExtends, lindenbaumIsFormal⟩
Proof state after:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
l₂ : ↑t ∩ generatedDisjunctions x = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions x)
l₄ : x ∈ generatedDisjunctions x
l₅ : lindenbaumExtension t (generatedDisjunctions x) ∩ generatedDisjunctions x = ∅
l₆ : x ∈ lindenbaumExtension t (generatedDisjunctions x)
⊢ False
Theorem: primeAnalysis
Proof state before:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
l₂ : ↑t ∩ generatedDisjunctions x = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions x)
l₄ : x ∈ generatedDisjunctions x
l₅ : lindenbaumExtension t (generatedDisjunctions x) ∩ generatedDisjunctions x = ∅
l₆ : x ∈ lindenbaumExtension t (generatedDisjunctions x)
⊢ False
Tactic:
exact Set.eq_empty_iff_forall_not_mem.mp l₅ x ⟨l₆,l₄⟩
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
⊢ ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
Tactic:
intros g h₃
Proof state after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
g : Form
h₃ : g ∈ generatedDisjunctions x
⊢ {g}⊢x
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
g : Form
h₃ : g ∈ generatedDisjunctions x
⊢ {g}⊢x
Tactic:
induction g
Proof state after:
case atom
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝ : ℕ
h₃ : #a✝ ∈ generatedDisjunctions x
⊢ {#a✝}⊢x

case neg
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝ : Form
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : ~a✝ ∈ generatedDisjunctions x
⊢ {~a✝}⊢x

case and
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝¹ a✝ : Form
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions x → {a✝¹}⊢x
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : a✝¹&a✝ ∈ generatedDisjunctions x
⊢ {a✝¹&a✝}⊢x

case or
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝¹ a✝ : Form
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions x → {a✝¹}⊢x
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : a✝¹¦a✝ ∈ generatedDisjunctions x
⊢ {a✝¹¦a✝}⊢x

case impl
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝¹ a✝ : Form
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions x → {a✝¹}⊢x
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : a✝¹⊃a✝ ∈ generatedDisjunctions x
⊢ {a✝¹⊃a✝}⊢x
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₃ : f¦g ∈ generatedDisjunctions x
⊢ {f¦g}⊢x
Tactic:
case or f g ih₁ ih₂ =>
  cases h₃
  case inl h₄ => rw [h₄]; exact ⟨BProof.ax rfl⟩
  case inr h₄ =>
    have ⟨prf₁⟩ := ih₁ h₄.left
    have ⟨prf₂⟩ := ih₂ h₄.right
    have thm₁ := BTheorem.mp (BTheorem.adj prf₁.toTheorem prf₂.toTheorem) BTheorem.orE
    exact ⟨thm₁.toProof ⟩
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
case atom
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝ : ℕ
h₃ : #a✝ ∈ generatedDisjunctions x
⊢ {#a✝}⊢x

case neg
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝ : Form
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : ~a✝ ∈ generatedDisjunctions x
⊢ {~a✝}⊢x

case and
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝¹ a✝ : Form
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions x → {a✝¹}⊢x
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : a✝¹&a✝ ∈ generatedDisjunctions x
⊢ {a✝¹&a✝}⊢x

case impl
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝¹ a✝ : Form
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions x → {a✝¹}⊢x
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : a✝¹⊃a✝ ∈ generatedDisjunctions x
⊢ {a✝¹⊃a✝}⊢x
Tactic:
all_goals
  cases h₃; exact ⟨BProof.ax rfl⟩
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₃ : f¦g ∈ generatedDisjunctions x
⊢ {f¦g}⊢x
Tactic:
cases h₃
Proof state after:
case inl
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h✝ : x = f¦g
⊢ {f¦g}⊢x

case inr
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h✝ : generatedDisjunctions x f ∧ generatedDisjunctions x g
⊢ {f¦g}⊢x
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : x = f¦g
⊢ {f¦g}⊢x
Tactic:
case inl h₄ => rw [h₄]; exact ⟨BProof.ax rfl⟩
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : generatedDisjunctions x f ∧ generatedDisjunctions x g
⊢ {f¦g}⊢x
Tactic:
case inr h₄ =>
  have ⟨prf₁⟩ := ih₁ h₄.left
  have ⟨prf₂⟩ := ih₂ h₄.right
  have thm₁ := BTheorem.mp (BTheorem.adj prf₁.toTheorem prf₂.toTheorem) BTheorem.orE
  exact ⟨thm₁.toProof ⟩
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : x = f¦g
⊢ {f¦g}⊢x
Tactic:
rw [h₄]
Proof state after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : x = f¦g
⊢ {f¦g}⊢f¦g
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : x = f¦g
⊢ {f¦g}⊢f¦g
Tactic:
exact ⟨BProof.ax rfl⟩
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : generatedDisjunctions x f ∧ generatedDisjunctions x g
⊢ {f¦g}⊢x
Tactic:
have ⟨prf₁⟩ := ih₁ h₄.left
Proof state after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : generatedDisjunctions x f ∧ generatedDisjunctions x g
prf₁ : BProof {f} x
⊢ {f¦g}⊢x
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : generatedDisjunctions x f ∧ generatedDisjunctions x g
prf₁ : BProof {f} x
⊢ {f¦g}⊢x
Tactic:
have ⟨prf₂⟩ := ih₂ h₄.right
Proof state after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : generatedDisjunctions x f ∧ generatedDisjunctions x g
prf₁ : BProof {f} x
prf₂ : BProof {g} x
⊢ {f¦g}⊢x
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : generatedDisjunctions x f ∧ generatedDisjunctions x g
prf₁ : BProof {f} x
prf₂ : BProof {g} x
⊢ {f¦g}⊢x
Tactic:
have thm₁ := BTheorem.mp (BTheorem.adj prf₁.toTheorem prf₂.toTheorem) BTheorem.orE
Proof state after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : generatedDisjunctions x f ∧ generatedDisjunctions x g
prf₁ : BProof {f} x
prf₂ : BProof {g} x
thm₁ : BTheorem (f¦g⊃x)
⊢ {f¦g}⊢x
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : generatedDisjunctions x f ∧ generatedDisjunctions x g
prf₁ : BProof {f} x
prf₂ : BProof {g} x
thm₁ : BTheorem (f¦g⊃x)
⊢ {f¦g}⊢x
Tactic:
exact ⟨thm₁.toProof ⟩
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
case impl
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝¹ a✝ : Form
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions x → {a✝¹}⊢x
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : a✝¹⊃a✝ ∈ generatedDisjunctions x
⊢ {a✝¹⊃a✝}⊢x
Tactic:
cases h₃
Proof state after:
case impl.refl
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹⊃a✝ ∈ ↑t
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions (a✝¹⊃a✝) → {a✝¹}⊢a✝¹⊃a✝
a_ih✝ : a✝ ∈ generatedDisjunctions (a✝¹⊃a✝) → {a✝}⊢a✝¹⊃a✝
⊢ {a✝¹⊃a✝}⊢a✝¹⊃a✝
Theorem: primeAnalysis
Proof state before:
case impl.refl
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹⊃a✝ ∈ ↑t
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions (a✝¹⊃a✝) → {a✝¹}⊢a✝¹⊃a✝
a_ih✝ : a✝ ∈ generatedDisjunctions (a✝¹⊃a✝) → {a✝}⊢a✝¹⊃a✝
⊢ {a✝¹⊃a✝}⊢a✝¹⊃a✝
Tactic:
exact ⟨BProof.ax rfl⟩
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
⊢ ↑t ∩ generatedDisjunctions x = ∅
Tactic:
apply Set.eq_empty_iff_forall_not_mem.mpr
Proof state after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
⊢ ∀ (x_1 : Form), ¬x_1 ∈ ↑t ∩ generatedDisjunctions x
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
⊢ ∀ (x_1 : Form), ¬x_1 ∈ ↑t ∩ generatedDisjunctions x
Tactic:
intros y h₃
Proof state after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
y : Form
h₃ : y ∈ ↑t ∩ generatedDisjunctions x
⊢ False
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
y : Form
h₃ : y ∈ ↑t ∩ generatedDisjunctions x
⊢ False
Tactic:
have ⟨prf₁⟩ := l₁ y h₃.right
Proof state after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
y : Form
h₃ : y ∈ ↑t ∩ generatedDisjunctions x
prf₁ : BProof {y} x
⊢ False
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
y : Form
h₃ : y ∈ ↑t ∩ generatedDisjunctions x
prf₁ : BProof {y} x
⊢ False
Tactic:
exact h₂ (t.property.mpr ⟨BProof.monotone (Set.singleton_subset_iff.mpr h₃.left) prf₁⟩)
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
l₂ : ↑t ∩ generatedDisjunctions x = ∅
⊢ isDisjunctionClosed (generatedDisjunctions x)
Tactic:
intros f g h₃
Proof state after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
l₂ : ↑t ∩ generatedDisjunctions x = ∅
f g : Form
h₃ : f ∈ generatedDisjunctions x ∧ g ∈ generatedDisjunctions x
⊢ f¦g ∈ generatedDisjunctions x
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
l₂ : ↑t ∩ generatedDisjunctions x = ∅
f g : Form
h₃ : f ∈ generatedDisjunctions x ∧ g ∈ generatedDisjunctions x
⊢ f¦g ∈ generatedDisjunctions x
Tactic:
exact Or.inr h₃
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
l₂ : ↑t ∩ generatedDisjunctions x = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions x)
⊢ x ∈ generatedDisjunctions x
Tactic:
cases x
Proof state after:
case atom
t : Th
a✝ : ℕ
h₁ : #a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬#a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions #a✝ → {g}⊢#a✝
l₂ : ↑t ∩ generatedDisjunctions #a✝ = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions #a✝)
⊢ #a✝ ∈ generatedDisjunctions #a✝

case neg
t : Th
a✝ : Form
h₁ : ~a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬~a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions ~a✝ → {g}⊢~a✝
l₂ : ↑t ∩ generatedDisjunctions ~a✝ = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions ~a✝)
⊢ ~a✝ ∈ generatedDisjunctions ~a✝

case and
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹&a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹&a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions (a✝¹&a✝) → {g}⊢a✝¹&a✝
l₂ : ↑t ∩ generatedDisjunctions (a✝¹&a✝) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (a✝¹&a✝))
⊢ a✝¹&a✝ ∈ generatedDisjunctions (a✝¹&a✝)

case or
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹¦a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹¦a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions (a✝¹¦a✝) → {g}⊢a✝¹¦a✝
l₂ : ↑t ∩ generatedDisjunctions (a✝¹¦a✝) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (a✝¹¦a✝))
⊢ a✝¹¦a✝ ∈ generatedDisjunctions (a✝¹¦a✝)

case impl
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹⊃a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions (a✝¹⊃a✝) → {g}⊢a✝¹⊃a✝
l₂ : ↑t ∩ generatedDisjunctions (a✝¹⊃a✝) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (a✝¹⊃a✝))
⊢ a✝¹⊃a✝ ∈ generatedDisjunctions (a✝¹⊃a✝)
Theorem: primeAnalysis
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬f¦g ∈ ↑t
l₁ : ∀ (g_1 : Form), g_1 ∈ generatedDisjunctions (f¦g) → {g_1}⊢f¦g
l₂ : ↑t ∩ generatedDisjunctions (f¦g) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (f¦g))
⊢ f¦g ∈ generatedDisjunctions (f¦g)
Tactic:
case or f g => exact Or.inl rfl
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
case atom
t : Th
a✝ : ℕ
h₁ : #a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬#a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions #a✝ → {g}⊢#a✝
l₂ : ↑t ∩ generatedDisjunctions #a✝ = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions #a✝)
⊢ #a✝ ∈ generatedDisjunctions #a✝

case neg
t : Th
a✝ : Form
h₁ : ~a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬~a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions ~a✝ → {g}⊢~a✝
l₂ : ↑t ∩ generatedDisjunctions ~a✝ = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions ~a✝)
⊢ ~a✝ ∈ generatedDisjunctions ~a✝

case and
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹&a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹&a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions (a✝¹&a✝) → {g}⊢a✝¹&a✝
l₂ : ↑t ∩ generatedDisjunctions (a✝¹&a✝) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (a✝¹&a✝))
⊢ a✝¹&a✝ ∈ generatedDisjunctions (a✝¹&a✝)

case impl
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹⊃a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions (a✝¹⊃a✝) → {g}⊢a✝¹⊃a✝
l₂ : ↑t ∩ generatedDisjunctions (a✝¹⊃a✝) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (a✝¹⊃a✝))
⊢ a✝¹⊃a✝ ∈ generatedDisjunctions (a✝¹⊃a✝)
Tactic:
all_goals 
  exact rfl
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬f¦g ∈ ↑t
l₁ : ∀ (g_1 : Form), g_1 ∈ generatedDisjunctions (f¦g) → {g_1}⊢f¦g
l₂ : ↑t ∩ generatedDisjunctions (f¦g) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (f¦g))
⊢ f¦g ∈ generatedDisjunctions (f¦g)
Tactic:
exact Or.inl rfl
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
case impl
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹⊃a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions (a✝¹⊃a✝) → {g}⊢a✝¹⊃a✝
l₂ : ↑t ∩ generatedDisjunctions (a✝¹⊃a✝) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (a✝¹⊃a✝))
⊢ a✝¹⊃a✝ ∈ generatedDisjunctions (a✝¹⊃a✝)
Tactic:
exact rfl
Proof state after:
no goals
Theorem: appBoundingFormalApplication
Proof state before:
⊢ ∀ (t u : Th) (p : Pr),
    formalApplicationFunction t u ≤ ↑p →
      ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Tactic:
intros t u p h₁
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Tactic:
have ⟨q,h₂,h₃⟩ := lemma1 t u p h₁
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
q : Pr
h₂ : t ≤ ↑q
h₃ : formalApplication ↑↑q ↑u ⊆ ↑↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
q : Pr
h₂ : t ≤ ↑q
h₃ : formalApplication ↑↑q ↑u ⊆ ↑↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Tactic:
have ⟨r,h₄,h₅⟩ := lemma2 t u p h₁
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
q : Pr
h₂ : t ≤ ↑q
h₃ : formalApplication ↑↑q ↑u ⊆ ↑↑p
r : Pr
h₄ : u ≤ ↑r
h₅ : formalApplication ↑t ↑↑r ⊆ ↑↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
q : Pr
h₂ : t ≤ ↑q
h₃ : formalApplication ↑↑q ↑u ⊆ ↑↑p
r : Pr
h₄ : u ≤ ↑r
h₅ : formalApplication ↑t ↑↑r ⊆ ↑↑p
⊢ ∃ q r, t ≤ ↑q ∧ u ≤ ↑r ∧ formalApplicationFunction (↑q) u ≤ ↑p ∧ formalApplicationFunction t ↑r ≤ ↑p
Tactic:
exact ⟨q,r,h₂,h₄,h₃,h₅⟩
Proof state after:
no goals
Theorem: appBoundingFormalApplication
Proof state before:
⊢ ∀ (t u : Th) (p : Pr), formalApplicationFunction t u ≤ ↑p → ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
intros t u p h₁
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
let Δ := {f : Form | ¬(formalApplication (▲{f}) u ⊆ p) }
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
have l₂ : ↑t ∩ Δ = ∅ := by
  apply Set.eq_empty_iff_forall_not_mem.mpr
  intros P h₂
  have l₃ : ▲{P} ⊆ ↑t := generatedContained (Set.singleton_subset_iff.mpr h₂.left)
  have l₄ := formalAppMonotoneRight ↑u l₃
  exact h₂.right $ le_trans l₄ h₁
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
have l₃ : isDisjunctionClosed Δ := by
  intros P Q h₁ h₂
  have ⟨R,l₄⟩ := nonconstruction h₁.left
  have ⟨⟨S,l₆,⟨prf₁⟩⟩,l₈⟩ := nonconstruction l₄
  have ⟨T,l₉⟩ := nonconstruction h₁.right
  have ⟨⟨U,l₁₀,⟨prf₂⟩⟩,l₁₂⟩ := nonconstruction l₉
  clear h₁ l₄ l₉
  have l₁₃ : ¬(R¦T ∈ p) := λw => Or.elim (p.property w) l₈ l₁₂
  apply l₁₃
  apply h₂
  clear l₈ l₁₂ l₁₃ h₂
  have prf₃ : BProof {P} (S & U ⊃ R ¦ T) := BProof.mp 
    (BProof.mp prf₁ (BTheorem.hs BTheorem.taut BTheorem.orI₁))
    (BTheorem.hs BTheorem.andE₁ BTheorem.taut)
  have prf₄ : BProof {Q} (S & U ⊃ R ¦ T) := BProof.mp 
    (BProof.mp prf₂ (BTheorem.hs BTheorem.taut BTheorem.orI₂))
    (BTheorem.hs BTheorem.andE₂ BTheorem.taut)
  have prf₅ : BProof {P ¦ Q} (S & U ⊃ R ¦ T) := BTheorem.toProof $
    BTheorem.mp (BTheorem.adj prf₃.toTheorem prf₄.toTheorem) BTheorem.orE
  clear prf₁ prf₂ prf₃ prf₄
  have l₁₄ : S & U ∈ u := u.property.mpr ⟨BProof.adj (BProof.ax l₆) (BProof.ax l₁₀)⟩
  exact ⟨S & U, l₁₄, ⟨prf₅⟩⟩
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p
Tactic:
have l₄ : lindenbaumExtension t Δ ∩ Δ = ∅  := lindenbaumTheorem l₂ l₃
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
l₂ : ↑t ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
l₄ : lindenbaumExtension t Δ ∩ Δ = ∅
⊢ ∃ q, t ≤ ↑q ∧ formalApplication ↑↑q ↑u ⊆ ↑↑p