internlm/Lean-Github huggingface dataset:
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
⊢ F ∈ fun f => ¬~f ∈ Γ
Tactic:
case mpr =>
  have ⟨prf₁⟩ := h₃
  induction prf₁
  case ax => assumption
  case mp P Q prf₂ thm₁ ih₁ =>
    intros h₄
    have l₁ := ih₁ ⟨prf₂⟩
    unfold FormalDual at l₁
    have thm₂ : BTheorem (~Q ⊃ ~P) := BTheorem.cp $ BTheorem.transitivity thm₁ (BTheorem.cp BTheorem.taut)
    have prf₂ := BProof.mp (BProof.ax h₄) thm₂
    exact l₁ (h₁.mpr ⟨prf₂⟩) 
  case adj P Q prf₁ prf₂ ih₁ ih₂ =>
    intros h₄
    have l₁ := ih₁ ⟨prf₁⟩
    have l₂ := ih₂ ⟨prf₂⟩
    have prf₃ := BProof.mp (BProof.ax h₄) BTheorem.demorgansLaw3
    have l₃ := h₂ (h₁.mpr ⟨prf₃⟩)
    cases l₃
    case inl left => exact l₁ left
    case inr right => exact l₂ right
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : F ∈ FormalDual Γ
⊢ (fun f => ¬~f ∈ Γ)⊢F
Tactic:
exact ⟨BProof.ax h₃⟩
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
⊢ F ∈ fun f => ¬~f ∈ Γ
Tactic:
have ⟨prf₁⟩ := h₃
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
prf₁ : BProof (FormalDual Γ) F
⊢ F ∈ fun f => ¬~f ∈ Γ
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
prf₁ : BProof (FormalDual Γ) F
⊢ F ∈ fun f => ¬~f ∈ Γ
Tactic:
induction prf₁
Proof state after:
case ax
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ : Form
h✝ : p✝ ∈ FormalDual Γ
h₃ : FormalDual Γ⊢p✝
⊢ p✝ ∈ fun f => ¬~f ∈ Γ

case mp
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ q✝ : Form
h₁✝ : BProof (FormalDual Γ) p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : FormalDual Γ⊢p✝ → p✝ ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢q✝
⊢ q✝ ∈ fun f => ¬~f ∈ Γ

case adj
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ q✝ : Form
h₁✝ : BProof (FormalDual Γ) p✝
h₂✝ : BProof (FormalDual Γ) q✝
h₁_ih✝ : FormalDual Γ⊢p✝ → p✝ ∈ fun f => ¬~f ∈ Γ
h₂_ih✝ : FormalDual Γ⊢q✝ → q✝ ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢p✝&q✝
⊢ p✝&q✝ ∈ fun f => ¬~f ∈ Γ
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ : Form
h✝ : p✝ ∈ FormalDual Γ
h₃ : FormalDual Γ⊢p✝
⊢ p✝ ∈ fun f => ¬~f ∈ Γ
Tactic:
case ax => assumption
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
⊢ Q ∈ fun f => ¬~f ∈ Γ
Tactic:
case mp P Q prf₂ thm₁ ih₁ =>
  intros h₄
  have l₁ := ih₁ ⟨prf₂⟩
  unfold FormalDual at l₁
  have thm₂ : BTheorem (~Q ⊃ ~P) := BTheorem.cp $ BTheorem.transitivity thm₁ (BTheorem.cp BTheorem.taut)
  have prf₂ := BProof.mp (BProof.ax h₄) thm₂
  exact l₁ (h₁.mpr ⟨prf₂⟩)
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
⊢ P&Q ∈ fun f => ¬~f ∈ Γ
Tactic:
case adj P Q prf₁ prf₂ ih₁ ih₂ =>
  intros h₄
  have l₁ := ih₁ ⟨prf₁⟩
  have l₂ := ih₂ ⟨prf₂⟩
  have prf₃ := BProof.mp (BProof.ax h₄) BTheorem.demorgansLaw3
  have l₃ := h₂ (h₁.mpr ⟨prf₃⟩)
  cases l₃
  case inl left => exact l₁ left
  case inr right => exact l₂ right
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ : Form
h✝ : p✝ ∈ FormalDual Γ
h₃ : FormalDual Γ⊢p✝
⊢ p✝ ∈ fun f => ¬~f ∈ Γ
Tactic:
assumption
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
⊢ Q ∈ fun f => ¬~f ∈ Γ
Tactic:
intros h₄
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
⊢ False
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
⊢ False
Tactic:
have l₁ := ih₁ ⟨prf₂⟩
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
⊢ False
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
⊢ False
Tactic:
have thm₂ : BTheorem (~Q ⊃ ~P) := BTheorem.cp $ BTheorem.transitivity thm₁ (BTheorem.cp BTheorem.taut)
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
thm₂ : BTheorem (~Q⊃~P)
⊢ False
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
thm₂ : BTheorem (~Q⊃~P)
⊢ False
Tactic:
have prf₂ := BProof.mp (BProof.ax h₄) thm₂
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂✝ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
thm₂ : BTheorem (~Q⊃~P)
prf₂ : BProof Γ ~P
⊢ False
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂✝ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
thm₂ : BTheorem (~Q⊃~P)
prf₂ : BProof Γ ~P
⊢ False
Tactic:
exact l₁ (h₁.mpr ⟨prf₂⟩)
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
⊢ P&Q ∈ fun f => ¬~f ∈ Γ
Tactic:
intros h₄
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
⊢ False
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
⊢ False
Tactic:
have l₁ := ih₁ ⟨prf₁⟩
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
⊢ False
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
⊢ False
Tactic:
have l₂ := ih₂ ⟨prf₂⟩
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
⊢ False
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
⊢ False
Tactic:
have prf₃ := BProof.mp (BProof.ax h₄) BTheorem.demorgansLaw3
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
⊢ False
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
⊢ False
Tactic:
have l₃ := h₂ (h₁.mpr ⟨prf₃⟩)
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
l₃ : ~P ∈ Γ ∨ ~Q ∈ Γ
⊢ False
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
l₃ : ~P ∈ Γ ∨ ~Q ∈ Γ
⊢ False
Tactic:
cases l₃
Proof state after:
case inl
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
h✝ : ~P ∈ Γ
⊢ False

case inr
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
h✝ : ~Q ∈ Γ
⊢ False
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
left : ~P ∈ Γ
⊢ False
Tactic:
case inl left => exact l₁ left
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
right : ~Q ∈ Γ
⊢ False
Tactic:
case inr right => exact l₂ right
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
left : ~P ∈ Γ
⊢ False
Tactic:
exact l₁ left
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
right : ~Q ∈ Γ
⊢ False
Tactic:
exact l₂ right
Proof state after:
no goals
Theorem: starInvolution
Proof state before:
⊢ Function.Involutive primeStarFunction
Tactic:
intros Γ
Proof state after:
Γ : Pr
⊢ primeStarFunction (primeStarFunction Γ) = Γ
Theorem: starInvolution
Proof state before:
Γ : Pr
⊢ primeStarFunction (primeStarFunction Γ) = Γ
Tactic:
ext f
Proof state after:
case a.a.h
Γ : Pr
f : Form
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ)) ↔ f ∈ ↑↑Γ
Theorem: starInvolution
Proof state before:
case a.a.h
Γ : Pr
f : Form
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ)) ↔ f ∈ ↑↑Γ
Tactic:
apply Iff.intro
Proof state after:
case a.a.h.mp
Γ : Pr
f : Form
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ)) → f ∈ ↑↑Γ

case a.a.h.mpr
Γ : Pr
f : Form
⊢ f ∈ ↑↑Γ → f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Theorem: starInvolution
Proof state before:
case a.a.h.mp
Γ : Pr
f : Form
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ)) → f ∈ ↑↑Γ

case a.a.h.mpr
Γ : Pr
f : Form
⊢ f ∈ ↑↑Γ → f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Tactic:
all_goals intros h₁
Proof state after:
case a.a.h.mp
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ f ∈ ↑↑Γ

case a.a.h.mpr
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Theorem: starInvolution
Proof state before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Tactic:
case a.a.h.mpr =>
  intros h₂
  have l₁ : ~~f ∈ Γ := Γ.val.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.dni⟩
  exact h₂ l₁
Proof state after:
no goals
Theorem: starInvolution
Proof state before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ f ∈ ↑↑Γ
Tactic:
case a.a.h.mp =>
  apply byContradiction
  intros h₂
  have l₂ : ¬(~~f ∈ Γ) := h₂ ∘ λel => Γ.val.property.mpr ⟨BProof.mp (BProof.ax el) BTheorem.dne⟩
  exact h₁ l₂
Proof state after:
no goals
Theorem: starInvolution
Proof state before:
case a.a.h.mpr
Γ : Pr
f : Form
⊢ f ∈ ↑↑Γ → f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Tactic:
intros h₁
Proof state after:
case a.a.h.mpr
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Theorem: starInvolution
Proof state before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
⊢ f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
Tactic:
intros h₂
Proof state after:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
h₂ : ~f ∈ ↑↑(primeStarFunction Γ)
⊢ False
Theorem: starInvolution
Proof state before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
h₂ : ~f ∈ ↑↑(primeStarFunction Γ)
⊢ False
Tactic:
have l₁ : ~~f ∈ Γ := Γ.val.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.dni⟩
Proof state after:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
h₂ : ~f ∈ ↑↑(primeStarFunction Γ)
l₁ : ~~f ∈ Γ
⊢ False
Theorem: starInvolution
Proof state before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑Γ
h₂ : ~f ∈ ↑↑(primeStarFunction Γ)
l₁ : ~~f ∈ Γ
⊢ False
Tactic:
exact h₂ l₁
Proof state after:
no goals
Theorem: starInvolution
Proof state before:
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ f ∈ ↑↑Γ
Tactic:
apply byContradiction
Proof state after:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ ¬f ∈ ↑↑Γ → False
Theorem: starInvolution
Proof state before:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
⊢ ¬f ∈ ↑↑Γ → False
Tactic:
intros h₂
Proof state after:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
h₂ : ¬f ∈ ↑↑Γ
⊢ False
Theorem: starInvolution
Proof state before:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
h₂ : ¬f ∈ ↑↑Γ
⊢ False
Tactic:
have l₂ : ¬(~~f ∈ Γ) := h₂ ∘ λel => Γ.val.property.mpr ⟨BProof.mp (BProof.ax el) BTheorem.dne⟩
Proof state after:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
h₂ : ¬f ∈ ↑↑Γ
l₂ : ¬~~f ∈ Γ
⊢ False
Theorem: starInvolution
Proof state before:
case h
Γ : Pr
f : Form
h₁ : f ∈ ↑↑(primeStarFunction (primeStarFunction Γ))
h₂ : ¬f ∈ ↑↑Γ
l₂ : ¬~~f ∈ Γ
⊢ False
Tactic:
exact h₁ l₂
Proof state after:
no goals
Theorem: starAntitone
Proof state before:
⊢ Antitone primeStarFunction
Tactic:
intros _ _ h₁ f h₂ h₃
Proof state after:
a✝ b✝ : Pr
h₁ : a✝ ≤ b✝
f : Form
h₂ : f ∈ (fun a => ↑a) ((fun a => ↑a) (primeStarFunction b✝))
h₃ : ~f ∈ ↑↑a✝
⊢ False
Theorem: starAntitone
Proof state before:
a✝ b✝ : Pr
h₁ : a✝ ≤ b✝
f : Form
h₂ : f ∈ (fun a => ↑a) ((fun a => ↑a) (primeStarFunction b✝))
h₃ : ~f ∈ ↑↑a✝
⊢ False
Tactic:
exact h₂ (h₁ h₃)
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
⊢ ∀ (t : Th), ↑t = ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
intros t
Proof state after:
t : Th
⊢ ↑t = ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Theorem: primeAnalysis
Proof state before:
t : Th
⊢ ↑t = ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
ext x
Proof state after:
case h
t : Th
x : Form
⊢ x ∈ ↑t ↔ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Theorem: primeAnalysis
Proof state before:
case h
t : Th
x : Form
⊢ x ∈ ↑t ↔ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
apply Iff.intro
Proof 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
Theorem: primeAnalysis
Proof 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₁
Proof state after:
no goals
Theorem: primeAnalysis
Proof 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₄⟩
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
⊢ x ∈ ↑t → x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
intros h₁
Proof state after:
t : Th
x : Form
h₁ : x ∈ ↑t
⊢ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ↑t
⊢ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
apply Set.mem_interₛ.mpr
Proof 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
Theorem: primeAnalysis
Proof 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₂
Proof state after:
t : Th
x : Form
h₁ : x ∈ ↑t
r : Set Form
h₂ : r ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ x ∈ r
Theorem: primeAnalysis
Proof 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₁
Proof state after:
no goals
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
⊢ x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → x ∈ ↑t
Tactic:
intros h₁
Proof state after:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ x ∈ ↑t
Theorem: primeAnalysis
Proof state before:
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ x ∈ ↑t
Tactic:
apply byContradiction
Proof state after:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ ¬x ∈ ↑t → False
Theorem: primeAnalysis
Proof state before:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ ¬x ∈ ↑t → False
Tactic:
intros h₂
Proof state after:
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
⊢ False
Theorem: primeAnalysis
Proof 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⟩
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
⊢ 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
⊢ 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₁⟩)
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 = ∅
⊢ 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 = ∅
⊢ False
Tactic:
have l₃ : isDisjunctionClosed (generatedDisjunctions x) := by
  intros f g h₃
  exact Or.inr h₃
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)
⊢ 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)
⊢ False
Tactic:
have l₄ : x ∈ generatedDisjunctions x := by 
  cases x
  case or f g => exact Or.inl rfl
  all_goals 
    exact rfl
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
⊢ False