internlm/Lean-Github huggingface dataset:
Theorem: logicInIdentity
Proof state before:
α : Type
inst : Model α
f g : Form
h₁ : Model.identity⊨f⊃g
x : α
h₂ : x⊨f
⊢ x⊨g
Tactic:
rw [←inst.appLeftIdent x]
Proof state after:
α : Type
inst : Model α
f g : Form
h₁ : Model.identity⊨f⊃g
x : α
h₂ : x⊨f
⊢ Model.identity∙x⊨g
Theorem: logicInIdentity
Proof state before:
α : Type
inst : Model α
f g : Form
h₁ : Model.identity⊨f⊃g
x : α
h₂ : x⊨f
⊢ Model.identity∙x⊨g
Tactic:
exact h₁ h₂
Proof state after:
no goals
Theorem: logicInIdentity
Proof state before:
α : Type
inst : Model α
f g : Form
⊢ (∀ (x : α), x⊨f → x⊨g) → Model.identity⊨f⊃g
Tactic:
intro h₁ u h₂
Proof state after:
α : Type
inst : Model α
f g : Form
h₁ : ∀ (x : α), x⊨f → x⊨g
u : α
h₂ : u⊨f
⊢ Model.identity∙u⊨g
Theorem: logicInIdentity
Proof state before:
α : Type
inst : Model α
f g : Form
h₁ : ∀ (x : α), x⊨f → x⊨g
u : α
h₂ : u⊨f
⊢ Model.identity∙u⊨g
Tactic:
rw [inst.appLeftIdent u]
Proof state after:
α : Type
inst : Model α
f g : Form
h₁ : ∀ (x : α), x⊨f → x⊨g
u : α
h₂ : u⊨f
⊢ u⊨g
Theorem: logicInIdentity
Proof state before:
α : Type
inst : Model α
f g : Form
h₁ : ∀ (x : α), x⊨f → x⊨g
u : α
h₂ : u⊨f
⊢ u⊨g
Tactic:
exact h₁ u h₂
Proof state after:
no goals
Theorem: starCompatLeft
Proof state before:
α : Type
inst : Model α
p : Model.primes
f : Form
⊢ ¬p⊨~f → p*⊨f
Tactic:
intros h₁
Proof state after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
⊢ p*⊨f
Theorem: starCompatLeft
Proof state before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
⊢ p*⊨f
Tactic:
have ⟨x, l₁⟩ := nonconstruction h₁
Proof state after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
⊢ p*⊨f
Theorem: starCompatLeft
Proof state before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
⊢ p*⊨f
Tactic:
have ⟨l₂,l₃⟩ := nonconstruction l₁
Proof state after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
⊢ p*⊨f
Theorem: starCompatLeft
Proof state before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
⊢ p*⊨f
Tactic:
have l₄ := byContradiction l₃
Proof state after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
l₄ : ↑(x*)⊨f
⊢ p*⊨f
Theorem: starCompatLeft
Proof state before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
l₄ : ↑(x*)⊨f
⊢ p*⊨f
Tactic:
have l₅ := inst.starAntitone l₂
Proof state after:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
l₄ : ↑(x*)⊨f
l₅ : x* ≤ p*
⊢ p*⊨f
Theorem: starCompatLeft
Proof state before:
α : Type
inst : Model α
p : Model.primes
f : Form
h₁ : ¬p⊨~f
x : Model.primes
l₁ : ¬(↑p ≤ ↑x → ¬↑(x*)⊨f)
l₂ : ↑p ≤ ↑x
l₃ : ¬¬↑(x*)⊨f
l₄ : ↑(x*)⊨f
l₅ : x* ≤ p*
⊢ p*⊨f
Tactic:
exact upwardsClosure l₅ l₄
Proof state after:
no goals
Theorem: generatedFormal
Proof state before:
⊢ ∀ (Γ : Ctx), formalTheory (▲Γ)
Tactic:
unfold formalTheory
Proof state after:
⊢ ∀ (Γ : Ctx) {f : Form}, f ∈ ▲Γ ↔ ▲Γ⊢f
Theorem: generatedFormal
Proof state before:
⊢ ∀ (Γ : Ctx) {f : Form}, f ∈ ▲Γ ↔ ▲Γ⊢f
Tactic:
intros Γ f
Proof state after:
Γ : Ctx
f : Form
⊢ f ∈ ▲Γ ↔ ▲Γ⊢f
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f : Form
⊢ f ∈ ▲Γ ↔ ▲Γ⊢f
Tactic:
apply Iff.intro
Proof state after:
case mp
Γ : Ctx
f : Form
⊢ f ∈ ▲Γ → ▲Γ⊢f

case mpr
Γ : Ctx
f : Form
⊢ ▲Γ⊢f → f ∈ ▲Γ
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f : Form
⊢ f ∈ ▲Γ → ▲Γ⊢f
Tactic:
case mp => 
   intros h₁
   exact Nonempty.intro $ BProof.ax h₁
Proof state after:
no goals
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f : Form
⊢ ▲Γ⊢f → f ∈ ▲Γ
Tactic:
case mpr =>
  intros h₁  
  have ⟨w⟩ := h₁
  induction w
  case ax => assumption
  case mp P Q prf thm ih => 
    have ⟨prf₂⟩ := ih ⟨prf⟩
    exact ⟨BProof.mp prf₂ thm⟩
  case adj P Q prf₁ prf₂ ih₁ ih₂ => 
    have ⟨prf₃⟩ := ih₁ ⟨prf₁⟩
    have ⟨prf₄⟩ := ih₂ ⟨prf₂⟩
    exact ⟨BProof.adj prf₃ prf₄⟩
Proof state after:
no goals
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f : Form
⊢ f ∈ ▲Γ → ▲Γ⊢f
Tactic:
intros h₁
Proof state after:
Γ : Ctx
f : Form
h₁ : f ∈ ▲Γ
⊢ ▲Γ⊢f
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f : Form
h₁ : f ∈ ▲Γ
⊢ ▲Γ⊢f
Tactic:
exact Nonempty.intro $ BProof.ax h₁
Proof state after:
no goals
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f : Form
⊢ ▲Γ⊢f → f ∈ ▲Γ
Tactic:
intros h₁
Proof state after:
Γ : Ctx
f : Form
h₁ : ▲Γ⊢f
⊢ f ∈ ▲Γ
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f : Form
h₁ : ▲Γ⊢f
⊢ f ∈ ▲Γ
Tactic:
have ⟨w⟩ := h₁
Proof state after:
Γ : Ctx
f : Form
h₁ : ▲Γ⊢f
w : BProof (▲Γ) f
⊢ f ∈ ▲Γ
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f : Form
h₁ : ▲Γ⊢f
w : BProof (▲Γ) f
⊢ f ∈ ▲Γ
Tactic:
induction w
Proof state after:
case ax
Γ : Ctx
f p✝ : Form
h✝ : p✝ ∈ ▲Γ
h₁ : ▲Γ⊢p✝
⊢ p✝ ∈ ▲Γ

case mp
Γ : Ctx
f p✝ q✝ : Form
h₁✝ : BProof (▲Γ) p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : ▲Γ⊢p✝ → p✝ ∈ ▲Γ
h₁ : ▲Γ⊢q✝
⊢ q✝ ∈ ▲Γ

case adj
Γ : Ctx
f p✝ q✝ : Form
h₁✝ : BProof (▲Γ) p✝
h₂✝ : BProof (▲Γ) q✝
h₁_ih✝ : ▲Γ⊢p✝ → p✝ ∈ ▲Γ
h₂_ih✝ : ▲Γ⊢q✝ → q✝ ∈ ▲Γ
h₁ : ▲Γ⊢p✝&q✝
⊢ p✝&q✝ ∈ ▲Γ
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f p✝ : Form
h✝ : p✝ ∈ ▲Γ
h₁ : ▲Γ⊢p✝
⊢ p✝ ∈ ▲Γ
Tactic:
case ax => assumption
Proof state after:
no goals
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f P Q : Form
prf : BProof (▲Γ) P
thm : BTheorem (P⊃Q)
ih : ▲Γ⊢P → P ∈ ▲Γ
h₁ : ▲Γ⊢Q
⊢ Q ∈ ▲Γ
Tactic:
case mp P Q prf thm ih => 
  have ⟨prf₂⟩ := ih ⟨prf⟩
  exact ⟨BProof.mp prf₂ thm⟩
Proof state after:
no goals
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
⊢ P&Q ∈ ▲Γ
Tactic:
case adj P Q prf₁ prf₂ ih₁ ih₂ => 
  have ⟨prf₃⟩ := ih₁ ⟨prf₁⟩
  have ⟨prf₄⟩ := ih₂ ⟨prf₂⟩
  exact ⟨BProof.adj prf₃ prf₄⟩
Proof state after:
no goals
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f p✝ : Form
h✝ : p✝ ∈ ▲Γ
h₁ : ▲Γ⊢p✝
⊢ p✝ ∈ ▲Γ
Tactic:
assumption
Proof state after:
no goals
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f P Q : Form
prf : BProof (▲Γ) P
thm : BTheorem (P⊃Q)
ih : ▲Γ⊢P → P ∈ ▲Γ
h₁ : ▲Γ⊢Q
⊢ Q ∈ ▲Γ
Tactic:
have ⟨prf₂⟩ := ih ⟨prf⟩
Proof state after:
Γ : Ctx
f P Q : Form
prf : BProof (▲Γ) P
thm : BTheorem (P⊃Q)
ih : ▲Γ⊢P → P ∈ ▲Γ
h₁ : ▲Γ⊢Q
prf₂ : BProof Γ P
⊢ Q ∈ ▲Γ
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f P Q : Form
prf : BProof (▲Γ) P
thm : BTheorem (P⊃Q)
ih : ▲Γ⊢P → P ∈ ▲Γ
h₁ : ▲Γ⊢Q
prf₂ : BProof Γ P
⊢ Q ∈ ▲Γ
Tactic:
exact ⟨BProof.mp prf₂ thm⟩
Proof state after:
no goals
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
⊢ P&Q ∈ ▲Γ
Tactic:
have ⟨prf₃⟩ := ih₁ ⟨prf₁⟩
Proof state after:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
prf₃ : BProof Γ P
⊢ P&Q ∈ ▲Γ
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
prf₃ : BProof Γ P
⊢ P&Q ∈ ▲Γ
Tactic:
have ⟨prf₄⟩ := ih₂ ⟨prf₂⟩
Proof state after:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
prf₃ : BProof Γ P
prf₄ : BProof Γ Q
⊢ P&Q ∈ ▲Γ
Theorem: generatedFormal
Proof state before:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
prf₃ : BProof Γ P
prf₄ : BProof Γ Q
⊢ P&Q ∈ ▲Γ
Tactic:
exact ⟨BProof.adj prf₃ prf₄⟩
Proof state after:
no goals
Theorem: generatedDisjunction
Proof state before:
f g h : Form
⊢ f ∈ ▲{g} ∧ f ∈ ▲{h} → f ∈ ▲{g¦h}
Tactic:
intros h₁
Proof state after:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
⊢ f ∈ ▲{g¦h}
Theorem: generatedDisjunction
Proof state before:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
⊢ f ∈ ▲{g¦h}
Tactic:
have ⟨⟨prf₁⟩,⟨prf₂⟩⟩ := h₁
Proof state after:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
⊢ f ∈ ▲{g¦h}
Theorem: generatedDisjunction
Proof state before:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
⊢ f ∈ ▲{g¦h}
Tactic:
have l₁ := prf₁.toTheorem
Proof state after:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
⊢ f ∈ ▲{g¦h}
Theorem: generatedDisjunction
Proof state before:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
⊢ f ∈ ▲{g¦h}
Tactic:
have l₂ := prf₂.toTheorem
Proof state after:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
l₂ : BTheorem (h⊃f)
⊢ f ∈ ▲{g¦h}
Theorem: generatedDisjunction
Proof state before:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
l₂ : BTheorem (h⊃f)
⊢ f ∈ ▲{g¦h}
Tactic:
have l₃ := (BTheorem.mp (BTheorem.adj l₁ l₂) BTheorem.orE)
Proof state after:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
l₂ : BTheorem (h⊃f)
l₃ : BTheorem (g¦h⊃f)
⊢ f ∈ ▲{g¦h}
Theorem: generatedDisjunction
Proof state before:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
l₂ : BTheorem (h⊃f)
l₃ : BTheorem (g¦h⊃f)
⊢ f ∈ ▲{g¦h}
Tactic:
exact ⟨l₃.toProof⟩
Proof state after:
no goals
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
⊢ Γ ⊆ ↑Δ → ▲Γ ⊆ ↑Δ
Tactic:
intros h₁ f h₂
Proof state after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f : Form
h₂ : f ∈ ▲Γ
⊢ f ∈ ↑Δ
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f : Form
h₂ : f ∈ ▲Γ
⊢ f ∈ ↑Δ
Tactic:
have ⟨prf⟩ := h₂
Proof state after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f : Form
h₂ : f ∈ ▲Γ
prf : BProof Γ f
⊢ f ∈ ↑Δ
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f : Form
h₂ : f ∈ ▲Γ
prf : BProof Γ f
⊢ f ∈ ↑Δ
Tactic:
induction prf
Proof state after:
case ax
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p✝ : Form
h✝ : p✝ ∈ Γ
h₂ : p✝ ∈ ▲Γ
⊢ p✝ ∈ ↑Δ

case mp
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p✝ q✝ : Form
h₁✝ : BProof Γ p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : p✝ ∈ ▲Γ → p✝ ∈ ↑Δ
h₂ : q✝ ∈ ▲Γ
⊢ q✝ ∈ ↑Δ

case adj
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p✝ q✝ : Form
h₁✝ : BProof Γ p✝
h₂✝ : BProof Γ q✝
h₁_ih✝ : p✝ ∈ ▲Γ → p✝ ∈ ↑Δ
h₂_ih✝ : q✝ ∈ ▲Γ → q✝ ∈ ↑Δ
h₂ : p✝&q✝ ∈ ▲Γ
⊢ p✝&q✝ ∈ ↑Δ
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p : Form
ih : p ∈ Γ
h₂ : p ∈ ▲Γ
⊢ p ∈ ↑Δ
Tactic:
case ax p ih => exact h₁ ih
Proof state after:
no goals
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
⊢ q ∈ ↑Δ
Tactic:
case mp p q prf₁ prf₂ ih => 
  have l₁ := ih ⟨prf₁⟩
  have ⟨prf₃⟩ := Δ.property.mp l₁
  exact Δ.property.mpr ⟨BProof.mp prf₃ prf₂⟩
Proof state after:
no goals
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
⊢ p&q ∈ ↑Δ
Tactic:
case adj p q prf₁ prf₂ ih₁ ih₂ => 
  have l₁ := ih₁ ⟨prf₁⟩
  have l₂ := ih₂ ⟨prf₂⟩
  have ⟨prf₃⟩ := Δ.property.mp l₁
  have ⟨prf₄⟩ := Δ.property.mp l₂
  exact Δ.property.mpr ⟨BProof.adj prf₃ prf₄⟩
Proof state after:
no goals
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p : Form
ih : p ∈ Γ
h₂ : p ∈ ▲Γ
⊢ p ∈ ↑Δ
Tactic:
exact h₁ ih
Proof state after:
no goals
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
⊢ q ∈ ↑Δ
Tactic:
have l₁ := ih ⟨prf₁⟩
Proof state after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
l₁ : p ∈ ↑Δ
⊢ q ∈ ↑Δ
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
l₁ : p ∈ ↑Δ
⊢ q ∈ ↑Δ
Tactic:
have ⟨prf₃⟩ := Δ.property.mp l₁
Proof state after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
l₁ : p ∈ ↑Δ
prf₃ : BProof (↑Δ) p
⊢ q ∈ ↑Δ
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
l₁ : p ∈ ↑Δ
prf₃ : BProof (↑Δ) p
⊢ q ∈ ↑Δ
Tactic:
exact Δ.property.mpr ⟨BProof.mp prf₃ prf₂⟩
Proof state after:
no goals
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
⊢ p&q ∈ ↑Δ
Tactic:
have l₁ := ih₁ ⟨prf₁⟩
Proof state after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
⊢ p&q ∈ ↑Δ
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
⊢ p&q ∈ ↑Δ
Tactic:
have l₂ := ih₂ ⟨prf₂⟩
Proof state after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
⊢ p&q ∈ ↑Δ
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
⊢ p&q ∈ ↑Δ
Tactic:
have ⟨prf₃⟩ := Δ.property.mp l₁
Proof state after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
prf₃ : BProof (↑Δ) p
⊢ p&q ∈ ↑Δ
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
prf₃ : BProof (↑Δ) p
⊢ p&q ∈ ↑Δ
Tactic:
have ⟨prf₄⟩ := Δ.property.mp l₂
Proof state after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
prf₃ : BProof (↑Δ) p
prf₄ : BProof (↑Δ) q
⊢ p&q ∈ ↑Δ
Theorem: generatedContained
Proof state before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
prf₃ : BProof (↑Δ) p
prf₄ : BProof (↑Δ) q
⊢ p&q ∈ ↑Δ
Tactic:
exact Δ.property.mpr ⟨BProof.adj prf₃ prf₄⟩
Proof state after:
no goals
Theorem: formalFixed
Proof state before:
Γ : Ctx
⊢ formalTheory Γ → ▲Γ = Γ
Tactic:
intros h₁
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
⊢ ▲Γ = Γ
Theorem: formalFixed
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
⊢ ▲Γ = Γ
Tactic:
funext
Proof state after:
case h
Γ : Ctx
h₁ : formalTheory Γ
x✝ : Form
⊢ (▲Γ) x✝ = Γ x✝
Theorem: formalFixed
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
x : Form
⊢ (▲Γ) x = Γ x
Tactic:
ext
Proof state after:
case a
Γ : Ctx
h₁ : formalTheory Γ
x : Form
⊢ (▲Γ) x ↔ Γ x
Theorem: formalFixed
Proof state before:
case a
Γ : Ctx
h₁ : formalTheory Γ
x : Form
⊢ (▲Γ) x ↔ Γ x
Tactic:
apply Iff.intro
Proof state after:
case a.mp
Γ : Ctx
h₁ : formalTheory Γ
x : Form
⊢ (▲Γ) x → Γ x

case a.mpr
Γ : Ctx
h₁ : formalTheory Γ
x : Form
⊢ Γ x → (▲Γ) x
Theorem: BisFormal
Proof state before:
⊢ formalTheory BTheory
Tactic:
intros f
Proof state after:
f : Form
⊢ f ∈ BTheory ↔ BTheory⊢f
Theorem: BisFormal
Proof state before:
f : Form
⊢ f ∈ BTheory ↔ BTheory⊢f
Tactic:
apply Iff.intro
Proof state after:
case mp
f : Form
⊢ f ∈ BTheory → BTheory⊢f

case mpr
f : Form
⊢ BTheory⊢f → f ∈ BTheory
Theorem: BisFormal
Proof state before:
f P Q : Form
prf₁ : BProof BTheory P
thm₁ : BTheorem (P⊃Q)
ih : BTheory⊢P → P ∈ BTheory
h₁ : BTheory⊢Q
⊢ Q ∈ BTheory
Tactic:
have l₁ := ih ⟨prf₁⟩
Proof state after:
f P Q : Form
prf₁ : BProof BTheory P
thm₁ : BTheorem (P⊃Q)
ih : BTheory⊢P → P ∈ BTheory
h₁ : BTheory⊢Q
l₁ : P ∈ BTheory
⊢ Q ∈ BTheory
Theorem: BisFormal
Proof state before:
f P Q : Form
prf₁ : BProof BTheory P
thm₁ : BTheorem (P⊃Q)
ih : BTheory⊢P → P ∈ BTheory
h₁ : BTheory⊢Q
l₁ : P ∈ BTheory
⊢ Q ∈ BTheory
Tactic:
have ⟨thm₂⟩ := l₁
Proof state after:
f P Q : Form
prf₁ : BProof BTheory P
thm₁ : BTheorem (P⊃Q)
ih : BTheory⊢P → P ∈ BTheory
h₁ : BTheory⊢Q
l₁ : P ∈ BTheory
thm₂ : BTheorem P
⊢ Q ∈ BTheory
Theorem: BisFormal
Proof state before:
f P Q : Form
prf₁ : BProof BTheory P
thm₁ : BTheorem (P⊃Q)
ih : BTheory⊢P → P ∈ BTheory
h₁ : BTheory⊢Q
l₁ : P ∈ BTheory
thm₂ : BTheorem P
⊢ Q ∈ BTheory
Tactic:
exact ⟨BTheorem.mp thm₂ thm₁⟩
Proof state after:
no goals
Theorem: BisFormal
Proof state before:
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
⊢ P&Q ∈ BTheory
Tactic:
have ⟨l₁⟩ := ih₁ ⟨prf₁⟩
Proof state after:
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
l₁ : BTheorem P
⊢ P&Q ∈ BTheory
Theorem: BisFormal
Proof state before:
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
l₁ : BTheorem P
⊢ P&Q ∈ BTheory
Tactic:
have ⟨l₂⟩ := ih₂ ⟨prf₂⟩
Proof state after:
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
l₁ : BTheorem P
l₂ : BTheorem Q
⊢ P&Q ∈ BTheory
Theorem: BisFormal
Proof state before:
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
l₁ : BTheorem P
l₂ : BTheorem Q
⊢ P&Q ∈ BTheory
Tactic:
exact ⟨BTheorem.adj l₁ l₂⟩
Proof state after:
no goals
Theorem: formalAppMonotoneLeft
Proof state before:
⊢ ∀ (Γ : Ctx), Monotone (formalApplication Γ)
Tactic:
intros Γ a b h₁ A h₂
Proof state after:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ formalApplication Γ a
⊢ A ∈ formalApplication Γ b
Theorem: formalAppMonotoneLeft
Proof state before:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ formalApplication Γ a
⊢ A ∈ formalApplication Γ b
Tactic:
have ⟨g,h₃⟩ := h₂
Proof state after:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ formalApplication Γ a
g : Form
h₃ : g ∈ a ∧ g⊃A ∈ Γ
⊢ A ∈ formalApplication Γ b
Theorem: formalAppMonotoneLeft
Proof state before:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ formalApplication Γ a
g : Form
h₃ : g ∈ a ∧ g⊃A ∈ Γ
⊢ A ∈ formalApplication Γ b
Tactic:
exact ⟨g, h₁ h₃.left, h₃.right⟩
Proof state after:
no goals
Theorem: formalAppMonotoneRight
Proof state before:
⊢ ∀ (Γ : Ctx), Monotone (flip formalApplication Γ)
Tactic:
intros Γ a b h₁ A h₂
Proof state after:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ flip formalApplication Γ a
⊢ A ∈ flip formalApplication Γ b
Theorem: formalAppMonotoneRight
Proof state before:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ flip formalApplication Γ a
⊢ A ∈ flip formalApplication Γ b
Tactic:
have ⟨g,h₃⟩ := h₂
Proof state after:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ flip formalApplication Γ a
g : Form
h₃ : g ∈ Γ ∧ g⊃A ∈ a
⊢ A ∈ flip formalApplication Γ b
Theorem: formalAppMonotoneRight
Proof state before:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ flip formalApplication Γ a
g : Form
h₃ : g ∈ Γ ∧ g⊃A ∈ a
⊢ A ∈ flip formalApplication Γ b
Tactic:
exact ⟨g, h₃.left, h₁ h₃.right⟩
Proof state after:
no goals
Theorem: formalAppFunctionMonotoneRight
Proof state before:
⊢ ∀ (Γ : Th), Monotone (flip formalApplicationFunction Γ)
Tactic:
intros Γ _ _ h₁
Proof state after:
Γ a✝ b✝ : Th
h₁ : a✝ ≤ b✝
⊢ flip formalApplicationFunction Γ a✝ ≤ flip formalApplicationFunction Γ b✝
Theorem: formalAppFunctionMonotoneRight
Proof state before:
Γ a✝ b✝ : Th
h₁ : a✝ ≤ b✝
⊢ flip formalApplicationFunction Γ a✝ ≤ flip formalApplicationFunction Γ b✝
Tactic:
exact formalAppMonotoneRight Γ h₁
Proof state after:
no goals
Theorem: formalAppFunctionMonotoneLeft
Proof state before:
⊢ ∀ (Γ : Th), Monotone (formalApplicationFunction Γ)
Tactic:
intros Γ _ _ h₁
Proof state after:
Γ a✝ b✝ : Th
h₁ : a✝ ≤ b✝
⊢ formalApplicationFunction Γ a✝ ≤ formalApplicationFunction Γ b✝
Theorem: formalAppFunctionMonotoneLeft
Proof state before:
Γ a✝ b✝ : Th
h₁ : a✝ ≤ b✝
⊢ formalApplicationFunction Γ a✝ ≤ formalApplicationFunction Γ b✝
Tactic:
exact formalAppMonotoneLeft Γ h₁
Proof state after:
no goals
Theorem: formalAppIdentLeft
Proof state before:
⊢ ∀ (Γ : Th), formalApplicationFunction BTh Γ = Γ
Tactic:
intros Γ
Proof state after:
Γ : Th
⊢ formalApplicationFunction BTh Γ = Γ
Theorem: formalAppIdentLeft
Proof state before:
Γ : Th
⊢ formalApplicationFunction BTh Γ = Γ
Tactic:
ext f
Proof state after:
case a.h
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) ↔ f ∈ ↑Γ
Theorem: formalAppIdentLeft
Proof state before:
case a.h
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) ↔ f ∈ ↑Γ
Tactic:
apply Iff.intro
Proof state after:
case a.h.mp
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) → f ∈ ↑Γ

case a.h.mpr
Γ : Th
f : Form
⊢ f ∈ ↑Γ → f ∈ ↑(formalApplicationFunction BTh Γ)
Theorem: formalAppIdentLeft
Proof state before:
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) → f ∈ ↑Γ
Tactic:
case a.h.mp =>
  intros h₁
  have ⟨g,h₂,⟨h₃⟩⟩ := h₁
  exact Γ.property.mpr ⟨BProof.mp (BProof.ax h₂) h₃⟩
Proof state after:
no goals
Theorem: formalAppIdentLeft
Proof state before:
Γ : Th
f : Form
⊢ f ∈ ↑Γ → f ∈ ↑(formalApplicationFunction BTh Γ)
Tactic:
case a.h.mpr =>
  intros h₁
  exact ⟨f, h₁, ⟨BTheorem.taut⟩⟩
Proof state after:
no goals
Theorem: formalAppIdentLeft
Proof state before:
Γ : Th
f : Form
⊢ f ∈ ↑(formalApplicationFunction BTh Γ) → f ∈ ↑Γ
Tactic:
intros h₁
Proof state after:
Γ : Th
f : Form
h₁ : f ∈ ↑(formalApplicationFunction BTh Γ)
⊢ f ∈ ↑Γ
Theorem: formalAppIdentLeft
Proof state before:
Γ : Th
f : Form
h₁ : f ∈ ↑(formalApplicationFunction BTh Γ)
⊢ f ∈ ↑Γ
Tactic:
have ⟨g,h₂,⟨h₃⟩⟩ := h₁
Proof state after:
Γ : Th
f : Form
h₁ : f ∈ ↑(formalApplicationFunction BTh Γ)
g : Form
h₂ : g ∈ ↑Γ
h₃ : BTheorem (g⊃f)
⊢ f ∈ ↑Γ
Theorem: formalAppIdentLeft
Proof state before:
Γ : Th
f : Form
h₁ : f ∈ ↑(formalApplicationFunction BTh Γ)
g : Form
h₂ : g ∈ ↑Γ
h₃ : BTheorem (g⊃f)
⊢ f ∈ ↑Γ
Tactic:
exact Γ.property.mpr ⟨BProof.mp (BProof.ax h₂) h₃⟩
Proof state after:
no goals
Theorem: formalAppIdentLeft
Proof state before:
Γ : Th
f : Form
⊢ f ∈ ↑Γ → f ∈ ↑(formalApplicationFunction BTh Γ)
Tactic:
intros h₁
Proof state after:
Γ : Th
f : Form
h₁ : f ∈ ↑Γ
⊢ f ∈ ↑(formalApplicationFunction BTh Γ)
Theorem: formalAppIdentLeft
Proof state before:
Γ : Th
f : Form
h₁ : f ∈ ↑Γ
⊢ f ∈ ↑(formalApplicationFunction BTh Γ)
Tactic:
exact ⟨f, h₁, ⟨BTheorem.taut⟩⟩
Proof state after:
no goals
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
⊢ formalTheory (FormalDual Γ)
Tactic:
intros F
Proof state after:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
⊢ F ∈ FormalDual Γ ↔ FormalDual Γ⊢F
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
⊢ F ∈ FormalDual Γ ↔ FormalDual Γ⊢F
Tactic:
apply Iff.intro <;> intros h₃ <;> unfold FormalDual
Proof state after:
case mp
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : F ∈ FormalDual Γ
⊢ (fun f => ¬~f ∈ Γ)⊢F

case mpr
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
⊢ F ∈ fun f => ¬~f ∈ Γ
Theorem: formalStarFormal
Proof state before:
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : F ∈ FormalDual Γ
⊢ (fun f => ¬~f ∈ Γ)⊢F
Tactic:
case mp => exact ⟨BProof.ax h₃⟩
Proof state after:
no goals