Theorem: primeAnalysis (Fine/SystemB/CanonicalModel.lean)

State before:
⊢ ∀ (t : Th), ↑t = ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
intros t
State after:
t : Th
⊢ ↑t = ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }

State before:
t : Th
⊢ ↑t = ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
ext x
State after:
case h
t : Th
x : Form
⊢ x ∈ ↑t ↔ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }

State before:
case h
t : Th
x : Form
⊢ x ∈ ↑t ↔ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
apply Iff.intro
State after:
case h.mp
t : Th
x : Form
⊢ x ∈ ↑t → x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }

case h.mpr
t : Th
x : Form
⊢ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → x ∈ ↑t

State before:
t : Th
x : Form
⊢ x ∈ ↑t → x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
case h.mp =>
  intros h₁
  apply Set.mem_interₛ.mpr
  intros r h₂
  exact h₂.right.left h₁
State after:
no goals

State before:
t : Th
x : Form
⊢ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → x ∈ ↑t
Tactic:
case h.mpr =>
  intros h₁
  apply byContradiction
  intros h₂
  have l₁ : ∀ g : Form, g ∈ generatedDisjunctions x → {g} ⊢ x := by
    intros g h₃
    induction g
    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 ⟩
    all_goals
      cases h₃; exact ⟨BProof.ax rfl⟩
  have l₂ : ↑t ∩ generatedDisjunctions x = ∅ := by
    apply Set.eq_empty_iff_forall_not_mem.mpr
    intros y h₃
    have ⟨prf₁⟩ := l₁ y h₃.right
    exact h₂ (t.property.mpr ⟨BProof.monotone (Set.singleton_subset_iff.mpr h₃.left) prf₁⟩)
  have l₃ : isDisjunctionClosed (generatedDisjunctions x) := by
    intros f g h₃
    exact Or.inr h₃
  have l₄ : x ∈ generatedDisjunctions x := by 
    cases x
    case or f g => exact Or.inl rfl
    all_goals 
      exact rfl
  have l₅ := lindenbaumTheorem l₂ l₃
  have l₆ := (Set.mem_interₛ.mp h₁) 
    (lindenbaumExtension t (generatedDisjunctions x)) 
    ⟨lindenbaumIsPrime, lindenbaumExtensionExtends, lindenbaumIsFormal⟩
  exact Set.eq_empty_iff_forall_not_mem.mp l₅ x ⟨l₆,l₄⟩
State after:
no goals

State before:
t : Th
x : Form
⊢ x ∈ ↑t → x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
intros h₁
State after:
t : Th
x : Form
h₁ : x ∈ ↑t
⊢ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }

State before:
t : Th
x : Form
h₁ : x ∈ ↑t
⊢ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
apply Set.mem_interₛ.mpr
State after:
t : Th
x : Form
h₁ : x ∈ ↑t
⊢ ∀ (t_1 : Set Form), t_1 ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → x ∈ t_1

State before:
t : Th
x : Form
h₁ : x ∈ ↑t
⊢ ∀ (t_1 : Set Form), t_1 ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → x ∈ t_1
Tactic:
intros r h₂
State after:
t : Th
x : Form
h₁ : x ∈ ↑t
r : Set Form
h₂ : r ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ x ∈ r

State before:
t : Th
x : Form
h₁ : x ∈ ↑t
r : Set Form
h₂ : r ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ x ∈ r
Tactic:
exact h₂.right.left h₁
State after:
no goals

State before:
t : Th
x : Form
⊢ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → x ∈ ↑t
Tactic:
intros h₁
State after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ x ∈ ↑t

State before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ x ∈ ↑t
Tactic:
apply byContradiction
State after:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ ¬x ∈ ↑t → False

State before:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ ¬x ∈ ↑t → False
Tactic:
intros h₂
State after:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
⊢ False

State before:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
⊢ False
Tactic:
have l₁ : ∀ g : Form, g ∈ generatedDisjunctions x → {g} ⊢ x := by
  intros g h₃
  induction g
  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 ⟩
  all_goals
    cases h₃; exact ⟨BProof.ax rfl⟩
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
⊢ False

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
⊢ False
Tactic:
have l₂ : ↑t ∩ generatedDisjunctions x = ∅ := by
  apply Set.eq_empty_iff_forall_not_mem.mpr
  intros y h₃
  have ⟨prf₁⟩ := l₁ y h₃.right
  exact h₂ (t.property.mpr ⟨BProof.monotone (Set.singleton_subset_iff.mpr h₃.left) prf₁⟩)
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 = ∅
⊢ False

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 = ∅
⊢ False
Tactic:
have l₃ : isDisjunctionClosed (generatedDisjunctions x) := by
  intros f g h₃
  exact Or.inr h₃
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)
⊢ False

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)
⊢ False
Tactic:
have l₄ : x ∈ generatedDisjunctions x := by 
  cases x
  case or f g => exact Or.inl rfl
  all_goals 
    exact rfl
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
⊢ False

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₃
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

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⟩
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

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₄⟩
State after:
no goals

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₃
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

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
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

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 ⟩
State after:
no goals

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⟩
State after:
no goals

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₃
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

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⟩
State after:
no goals

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 ⟩
State after:
no goals

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₄]
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

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⟩
State after:
no goals

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
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

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
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

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
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

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 ⟩
State after:
no goals

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₃
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✝

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⟩
State after:
no goals

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
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

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₃
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

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
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

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₁⟩)
State after:
no goals

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₃
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

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₃
State after:
no goals

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
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✝)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals