internlm/Lean-Github huggingface dataset:
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ↑t
⊢ t⊨f¦g
Tactic:
case or.mpr f g =>
  intros p h₂
  rw [primeAnalysis] at h₁
  have l₁ : f ¦ g ∈ p.val.val := (Set.mem_interₛ.mp h₁ p) ⟨p.property, h₂, p.val.property⟩
  have l₂ : f ∈ p.val.val ∨ g ∈ p.val.val := p.property l₁
  cases l₂
  case inl h₂ => exact Or.inl $ canonicalSatisfaction.mpr h₂
  case inr h₂ => exact Or.inr $ canonicalSatisfaction.mpr h₂
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : t⊨~f
⊢ ~f ∈ ↑t
Tactic:
case neg.mp f => 
  rw [primeAnalysis]
  intros p h₂
  let pr : Pr := ⟨⟨p, h₂.right.right⟩,h₂.left⟩
  have l₁ := @h₁ pr h₂.right.left
  have l₂ := l₁ ∘ canonicalSatisfaction.mpr 
  apply byContradiction
  exact l₂
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : ~f ∈ ↑t
⊢ t⊨~f
Tactic:
case neg.mpr f => 
  intros p h₂ h₃
  rw [primeAnalysis] at h₁
  have l₁ : ~f ∈ p.val.val := (Set.mem_interₛ.mp h₁ p) ⟨p.property, h₂, p.val.property⟩
  exact canonicalSatisfaction.mp h₃ l₁
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f⊃g
⊢ f⊃g ∈ ↑t
Tactic:
case impl.mp f g =>
  apply byContradiction
  intros h₂
  let Δ : Th := ⟨▲{f}, generatedFormal {f}⟩
  have l₁ : ¬(g ∈ (formalApplicationFunction t Δ).val) := by
    intros h₃
    have ⟨q,⟨prf₁⟩,l₂⟩ := h₃
    have ⟨prf₂⟩ := t.property.mp l₂
    have prf₃ := BProof.mp prf₂ (BTheorem.hs prf₁.toTheorem BTheorem.taut)
    exact h₂ $ t.property.mpr ⟨prf₃⟩
  have l₂ : Δ ⊨ f := canonicalSatisfaction.mpr ⟨BProof.ax rfl⟩
  exact l₁ $ canonicalSatisfaction.mp (h₁ l₂)
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
⊢ t⊨f⊃g
Tactic:
case impl.mpr f g => 
  intros r h₂
  have l₁ := canonicalSatisfaction.mp h₂
  have l₂ : g ∈ (formalApplicationFunction t r).val := ⟨f, l₁, h₁⟩
  exact canonicalSatisfaction.mpr l₂
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
case impl
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹⊃a✝ ↔ a✝¹⊃a✝ ∈ ↑t
Tactic:
apply Iff.intro <;> intros h₁
Proof state after:
case impl.mp
t : Th
a✝¹ a✝ : Form
h₁ : t⊨a✝¹⊃a✝
⊢ a✝¹⊃a✝ ∈ ↑t

case impl.mpr
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ↑t
⊢ t⊨a✝¹⊃a✝
Theorem: canonicalSatisfaction
Proof state before:
t : Th
a✝ : ℕ
h₁ : t⊨#a✝
⊢ #a✝ ∈ ↑t
Tactic:
exact h₁
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
a✝ : ℕ
h₁ : #a✝ ∈ ↑t
⊢ t⊨#a✝
Tactic:
exact h₁
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f&g
⊢ f&g ∈ ↑t
Tactic:
have l₁ : f ∈ t := canonicalSatisfaction.mp h₁.left
Proof state after:
t : Th
f g : Form
h₁ : t⊨f&g
l₁ : f ∈ t
⊢ f&g ∈ ↑t
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f&g
l₁ : f ∈ t
⊢ f&g ∈ ↑t
Tactic:
have l₂ : g ∈ t := canonicalSatisfaction.mp h₁.right
Proof state after:
t : Th
f g : Form
h₁ : t⊨f&g
l₁ : f ∈ t
l₂ : g ∈ t
⊢ f&g ∈ ↑t
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f&g
l₁ : f ∈ t
l₂ : g ∈ t
⊢ f&g ∈ ↑t
Tactic:
exact t.property.mpr ⟨BProof.adj (BProof.ax l₁) (BProof.ax l₂)⟩
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
⊢ t⊨f&g
Tactic:
have l₁ : t ⊨ f := canonicalSatisfaction.mpr $ t.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.andE₁⟩
Proof state after:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
l₁ : t⊨f
⊢ t⊨f&g
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
l₁ : t⊨f
⊢ t⊨f&g
Tactic:
have l₂ : t ⊨ g := canonicalSatisfaction.mpr $ t.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.andE₂⟩
Proof state after:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
l₁ : t⊨f
l₂ : t⊨g
⊢ t⊨f&g
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f&g ∈ ↑t
l₁ : t⊨f
l₂ : t⊨g
⊢ t⊨f&g
Tactic:
exact ⟨l₁,l₂⟩
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
⊢ f¦g ∈ ↑t
Tactic:
rw [primeAnalysis]
Proof state after:
t : Th
f g : Form
h₁ : t⊨f¦g
⊢ f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
⊢ f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
intros p h₂
Proof state after:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ f¦g ∈ p
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ f¦g ∈ p
Tactic:
let pr : Pr := ⟨⟨p, h₂.right.right⟩,h₂.left⟩
Proof state after:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
⊢ f¦g ∈ p
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
⊢ f¦g ∈ p
Tactic:
have l₁ := @h₁ pr h₂.right.left
Proof state after:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ↑pr⊨f ∨ ↑pr⊨g
⊢ f¦g ∈ p
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ↑pr⊨f ∨ ↑pr⊨g
⊢ f¦g ∈ p
Tactic:
cases l₁
Proof state after:
case inl
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h✝ : ↑pr⊨f
⊢ f¦g ∈ p

case inr
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h✝ : ↑pr⊨g
⊢ f¦g ∈ p
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨f
⊢ f¦g ∈ p
Tactic:
case inl h₃ => 
  have l₂ := canonicalSatisfaction.mp h₃
  exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₁⟩
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨g
⊢ f¦g ∈ p
Tactic:
case inr h₃ => 
  have l₂ := canonicalSatisfaction.mp h₃
  exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₂⟩
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨f
⊢ f¦g ∈ p
Tactic:
have l₂ := canonicalSatisfaction.mp h₃
Proof state after:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨f
l₂ : f ∈ ↑↑pr
⊢ f¦g ∈ p
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨f
l₂ : f ∈ ↑↑pr
⊢ f¦g ∈ p
Tactic:
exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₁⟩
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨g
⊢ f¦g ∈ p
Tactic:
have l₂ := canonicalSatisfaction.mp h₃
Proof state after:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨g
l₂ : g ∈ ↑↑pr
⊢ f¦g ∈ p
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨g
l₂ : g ∈ ↑↑pr
⊢ f¦g ∈ p
Tactic:
exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₂⟩
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ↑t
⊢ t⊨f¦g
Tactic:
intros p h₂
Proof state after:
t : Th
f g : Form
h₁ : f¦g ∈ ↑t
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ↑t
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
rw [primeAnalysis] at h₁
Proof state after:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
have l₁ : f ¦ g ∈ p.val.val := (Set.mem_interₛ.mp h₁ p) ⟨p.property, h₂, p.val.property⟩
Proof state after:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
have l₂ : f ∈ p.val.val ∨ g ∈ p.val.val := p.property l₁
Proof state after:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
l₂ : f ∈ ↑↑p ∨ g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
l₂ : f ∈ ↑↑p ∨ g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
cases l₂
Proof state after:
case inl
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h✝ : f ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g

case inr
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h✝ : g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂✝ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h₂ : f ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
case inl h₂ => exact Or.inl $ canonicalSatisfaction.mpr h₂
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂✝ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h₂ : g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
case inr h₂ => exact Or.inr $ canonicalSatisfaction.mpr h₂
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂✝ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h₂ : f ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
exact Or.inl $ canonicalSatisfaction.mpr h₂
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂✝ : t ≤ ↑p
l₁ : f¦g ∈ ↑↑p
h₂ : g ∈ ↑↑p
⊢ ↑p⊨f ∨ ↑p⊨g
Tactic:
exact Or.inr $ canonicalSatisfaction.mpr h₂
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : t⊨~f
⊢ ~f ∈ ↑t
Tactic:
rw [primeAnalysis]
Proof state after:
t : Th
f : Form
h₁ : t⊨~f
⊢ ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : t⊨~f
⊢ ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
intros p h₂
Proof state after:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ ~f ∈ p
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ ~f ∈ p
Tactic:
let pr : Pr := ⟨⟨p, h₂.right.right⟩,h₂.left⟩
Proof state after:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
⊢ ~f ∈ p
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
⊢ ~f ∈ p
Tactic:
have l₁ := @h₁ pr h₂.right.left
Proof state after:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
⊢ ~f ∈ p
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
⊢ ~f ∈ p
Tactic:
have l₂ := l₁ ∘ canonicalSatisfaction.mpr
Proof state after:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
l₂ : f ∈ ↑↑(pr*) → False
⊢ ~f ∈ p
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
l₂ : f ∈ ↑↑(pr*) → False
⊢ ~f ∈ p
Tactic:
apply byContradiction
Proof state after:
case h
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
l₂ : f ∈ ↑↑(pr*) → False
⊢ ¬~f ∈ p → False
Theorem: canonicalSatisfaction
Proof state before:
case h
t : Th
f : Form
h₁ : t⊨~f
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
l₁ : ¬↑(pr*)⊨f
l₂ : f ∈ ↑↑(pr*) → False
⊢ ¬~f ∈ p → False
Tactic:
exact l₂
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : ~f ∈ ↑t
⊢ t⊨~f
Tactic:
intros p h₂ h₃
Proof state after:
t : Th
f : Form
h₁ : ~f ∈ ↑t
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : ~f ∈ ↑t
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False
Tactic:
rw [primeAnalysis] at h₁
Proof state after:
t : Th
f : Form
h₁ : ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
⊢ False
Tactic:
have l₁ : ~f ∈ p.val.val := (Set.mem_interₛ.mp h₁ p) ⟨p.property, h₂, p.val.property⟩
Proof state after:
t : Th
f : Form
h₁ : ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
l₁ : ~f ∈ ↑↑p
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
h₁ : ~f ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
p : Model.primes
h₂ : t ≤ ↑p
h₃ : ↑(p*)⊨f
l₁ : ~f ∈ ↑↑p
⊢ False
Tactic:
exact canonicalSatisfaction.mp h₃ l₁
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f⊃g
⊢ f⊃g ∈ ↑t
Tactic:
apply byContradiction
Proof state after:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
⊢ ¬f⊃g ∈ ↑t → False
Theorem: canonicalSatisfaction
Proof state before:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
⊢ ¬f⊃g ∈ ↑t → False
Tactic:
intros h₂
Proof state after:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
⊢ False
Tactic:
let Δ : Th := ⟨▲{f}, generatedFormal {f}⟩
Proof state after:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
⊢ False
Tactic:
have l₁ : ¬(g ∈ (formalApplicationFunction t Δ).val) := by
  intros h₃
  have ⟨q,⟨prf₁⟩,l₂⟩ := h₃
  have ⟨prf₂⟩ := t.property.mp l₂
  have prf₃ := BProof.mp prf₂ (BTheorem.hs prf₁.toTheorem BTheorem.taut)
  exact h₂ $ t.property.mpr ⟨prf₃⟩
Proof state after:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
l₁ : ¬g ∈ ↑(formalApplicationFunction t Δ)
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
l₁ : ¬g ∈ ↑(formalApplicationFunction t Δ)
⊢ False
Tactic:
have l₂ : Δ ⊨ f := canonicalSatisfaction.mpr ⟨BProof.ax rfl⟩
Proof state after:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
l₁ : ¬g ∈ ↑(formalApplicationFunction t Δ)
l₂ : Δ⊨f
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
case h
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
l₁ : ¬g ∈ ↑(formalApplicationFunction t Δ)
l₂ : Δ⊨f
⊢ False
Tactic:
exact l₁ $ canonicalSatisfaction.mp (h₁ l₂)
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
⊢ ¬g ∈ ↑(formalApplicationFunction t Δ)
Tactic:
intros h₃
Proof state after:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
⊢ False
Tactic:
have ⟨q,⟨prf₁⟩,l₂⟩ := h₃
Proof state after:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
⊢ False
Tactic:
have ⟨prf₂⟩ := t.property.mp l₂
Proof state after:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
prf₂ : BProof (↑t) (q⊃g)
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
prf₂ : BProof (↑t) (q⊃g)
⊢ False
Tactic:
have prf₃ := BProof.mp prf₂ (BTheorem.hs prf₁.toTheorem BTheorem.taut)
Proof state after:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
prf₂ : BProof (↑t) (q⊃g)
prf₃ : BProof (↑t) (f⊃g)
⊢ False
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
prf₂ : BProof (↑t) (q⊃g)
prf₃ : BProof (↑t) (f⊃g)
⊢ False
Tactic:
exact h₂ $ t.property.mpr ⟨prf₃⟩
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
⊢ t⊨f⊃g
Tactic:
intros r h₂
Proof state after:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
⊢ t∙r⊨g
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
⊢ t∙r⊨g
Tactic:
have l₁ := canonicalSatisfaction.mp h₂
Proof state after:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
l₁ : f ∈ ↑r
⊢ t∙r⊨g
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
l₁ : f ∈ ↑r
⊢ t∙r⊨g
Tactic:
have l₂ : g ∈ (formalApplicationFunction t r).val := ⟨f, l₁, h₁⟩
Proof state after:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
l₁ : f ∈ ↑r
l₂ : g ∈ ↑(formalApplicationFunction t r)
⊢ t∙r⊨g
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f g : Form
h₁ : f⊃g ∈ ↑t
r : Th
h₂ : r⊨f
l₁ : f ∈ ↑r
l₂ : g ∈ ↑(formalApplicationFunction t r)
⊢ t∙r⊨g
Tactic:
exact canonicalSatisfaction.mpr l₂
Proof state after:
no goals
Theorem: lindenbaumSequenceMonotone'
Proof state before:
t : Th
Δ : Ctx
⊢ ∀ (b a : Lex (ℕ × ℕ)), a ≤ b → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ b
Tactic:
intros b
Proof state after:
t : Th
Δ : Ctx
b : Lex (ℕ × ℕ)
⊢ ∀ (a : Lex (ℕ × ℕ)), a ≤ b → lindenbaumSequence t Δ a ⊆ lindenbaumSequence t Δ b