internlm/Lean-Github huggingface dataset:
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
l₃ : isDisjunctionClosed Δ
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Tactic:
clear l₂ l₃
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
Tactic:
refine ⟨⟨⟨lindenbaumExtension u Δ, lindenbaumIsFormal⟩, lindenbaumIsPrime⟩, lindenbaumExtensionExtends, ?_⟩
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ formalApplication ↑t
      ↑↑{
            val :=
              { val := lindenbaumExtension u Δ,
                property := (_ : ∀ {f : Form}, f ∈ lindenbaumExtension u Δ ↔ lindenbaumExtension u Δ⊢f) },
            property :=
              (_ :
                ∀ {f g : Form},
                  f¦g ∈ lindenbaumExtension u Δ → f ∈ lindenbaumExtension u Δ ∨ g ∈ lindenbaumExtension u Δ) } ⊆
    ↑↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ formalApplication ↑t
      ↑↑{
            val :=
              { val := lindenbaumExtension u Δ,
                property := (_ : ∀ {f : Form}, f ∈ lindenbaumExtension u Δ ↔ lindenbaumExtension u Δ⊢f) },
            property :=
              (_ :
                ∀ {f g : Form},
                  f¦g ∈ lindenbaumExtension u Δ → f ∈ lindenbaumExtension u Δ ∨ g ∈ lindenbaumExtension u Δ) } ⊆
    ↑↑p
Tactic:
change formalApplication ↑t (lindenbaumExtension u Δ) ⊆ p
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ formalApplication (↑t) (lindenbaumExtension u Δ) ⊆ ↑↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ formalApplication (↑t) (lindenbaumExtension u Δ) ⊆ ↑↑p
Tactic:
intros P h₁
Proof state after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
⊢ P ∈ ↑↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
⊢ P ∈ ↑↑p
Tactic:
have ⟨Q,h₂,h₃⟩ := h₁
Proof state after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ P ∈ ↑↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ P ∈ ↑↑p
Tactic:
have l₄ : formalApplication ↑t (▲{Q}) ⊆ ↑↑p := by
  apply byContradiction
  intros h₄
  exact (Set.eq_empty_iff_forall_not_mem.mp l₄) Q ⟨h₂,h₄⟩
Proof state after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄✝ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
l₄ : formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
⊢ P ∈ ↑↑p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄✝ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
l₄ : formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
⊢ P ∈ ↑↑p
Tactic:
exact l₄ ⟨Q,⟨BProof.ax rfl⟩,h₃⟩
Proof state after:
no goals
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
⊢ ↑u ∩ Δ = ∅
Tactic:
apply Set.eq_empty_iff_forall_not_mem.mpr
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
⊢ ∀ (x : Form), ¬x ∈ ↑u ∩ Δ
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
⊢ ∀ (x : Form), ¬x ∈ ↑u ∩ Δ
Tactic:
intros P h₂
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
⊢ False
Tactic:
have l₃ : ▲{P} ⊆ ↑u := generatedContained (Set.singleton_subset_iff.mpr h₂.left)
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
l₃ : ▲{P} ⊆ ↑u
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
l₃ : ▲{P} ⊆ ↑u
⊢ False
Tactic:
have l₄ := formalAppMonotoneLeft ↑t l₃
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
l₃ : ▲{P} ⊆ ↑u
l₄ : formalApplication (↑t) (▲{P}) ≤ formalApplication ↑t ↑u
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑u ∩ Δ
l₃ : ▲{P} ⊆ ↑u
l₄ : formalApplication (↑t) (▲{P}) ≤ formalApplication ↑t ↑u
⊢ False
Tactic:
exact h₂.right $ le_trans l₄ h₁
Proof state after:
no goals
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
⊢ isDisjunctionClosed Δ
Tactic:
intros P Q h₁ h₂
Proof state after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
⊢ False
Tactic:
have ⟨R,l₄⟩ := nonconstruction h₁.left
Proof state after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
⊢ False
Tactic:
have ⟨⟨S,⟨prf₁⟩,l₆⟩,l₈⟩ := nonconstruction l₄
Proof state after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
⊢ False
Tactic:
have ⟨T,l₉⟩ := nonconstruction h₁.right
Proof state after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (↑t) (▲{Q}) → T ∈ ↑↑p)
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (↑t) (▲{Q}) → T ∈ ↑↑p)
⊢ False
Tactic:
have ⟨⟨U,⟨prf₂⟩,l₁₀⟩,l₁₂⟩ := nonconstruction l₉
Proof state after:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (↑t) (▲{Q}) → T ∈ ↑↑p)
U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (↑t) (▲{Q}) → T ∈ ↑↑p)
U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
⊢ False
Tactic:
clear h₁ l₄ l₉
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
⊢ False
Tactic:
have l₁₃ : ¬(R¦T ∈ p) := λw => Or.elim (p.property w) l₈ l₁₂
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ False
Tactic:
apply l₁₃
Proof state after:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ p
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ p
Tactic:
apply h₂
Proof state after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Theorem: appBoundingFormalApplication
Proof state before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
l₁₃ : ¬R¦T ∈ p
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Tactic:
clear l₈ l₁₂ l₁₃ h₂
Proof state after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Theorem: appBoundingFormalApplication
Proof state before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Tactic:
have l₁₄ : S¦U ∈ ▲{P¦Q} := ⟨(BTheorem.orFunctor prf₁.toTheorem prf₂.toTheorem).toProof⟩
Proof state after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₄ : S¦U ∈ ▲{P¦Q}
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Theorem: appBoundingFormalApplication
Proof state before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₄ : S¦U ∈ ▲{P¦Q}
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Tactic:
have l₁₅ : (S¦U ⊃ R¦T) ∈ t := t.property.mpr ⟨BProof.mp (BProof.adj 
  (BProof.mp (BProof.ax l₆) (BTheorem.hs BTheorem.taut BTheorem.orI₁))
  (BProof.mp (BProof.ax l₁₀) (BTheorem.hs BTheorem.taut BTheorem.orI₂)))
  BTheorem.orE⟩
Proof state after:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₄ : S¦U ∈ ▲{P¦Q}
l₁₅ : S¦U⊃R¦T ∈ t
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Theorem: appBoundingFormalApplication
Proof state before:
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₄ : S¦U ∈ ▲{P¦Q}
l₁₅ : S¦U⊃R¦T ∈ t
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
Tactic:
exact ⟨S ¦ U, l₁₄, l₁₅⟩
Proof state after:
no goals
Theorem: appBoundingFormalApplication
Proof state before:
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
Tactic:
apply byContradiction
Proof state after:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ ¬formalApplication (↑t) (▲{Q}) ⊆ ↑↑p → False
Theorem: appBoundingFormalApplication
Proof state before:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
⊢ ¬formalApplication (↑t) (▲{Q}) ⊆ ↑↑p → False
Tactic:
intros h₄
Proof state after:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
h₄ : ¬formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
⊢ False
Theorem: appBoundingFormalApplication
Proof state before:
case h
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
P : Form
h₁ : P ∈ formalApplication (↑t) (lindenbaumExtension u Δ)
Q : Form
h₂ : Q ∈ lindenbaumExtension u Δ
h₃ : Q⊃P ∈ ↑t
h₄ : ¬formalApplication (↑t) (▲{Q}) ⊆ ↑↑p
⊢ False
Tactic:
exact (Set.eq_empty_iff_forall_not_mem.mp l₄) Q ⟨h₂,h₄⟩
Proof state after:
no goals
Theorem: theoryValuationMonotone
Proof state before:
⊢ Monotone theoryValuation
Tactic:
intros _ _ h₁ n h₂
Proof state after:
a✝ b✝ : Th
h₁ : a✝ ≤ b✝
n : ℕ
h₂ : n ∈ theoryValuation a✝
⊢ n ∈ theoryValuation b✝
Theorem: theoryValuationMonotone
Proof state before:
a✝ b✝ : Th
h₁ : a✝ ≤ b✝
n : ℕ
h₂ : n ∈ theoryValuation a✝
⊢ n ∈ theoryValuation b✝
Tactic:
exact h₁ h₂
Proof state after:
no goals
Theorem: theoryValuationBounding
Proof state before:
⊢ ∀ (t : Th) (x : ℕ), (∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p) → x ∈ theoryValuation t
Tactic:
intros t x h₁
Proof state after:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ x ∈ theoryValuation t
Theorem: theoryValuationBounding
Proof state before:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ x ∈ theoryValuation t
Tactic:
change #x ∈ t.val
Proof state after:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ #x ∈ ↑t
Theorem: theoryValuationBounding
Proof state before:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ #x ∈ ↑t
Tactic:
rw [primeAnalysis t]
Proof state after:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ #x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Theorem: theoryValuationBounding
Proof state before:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ #x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
Tactic:
apply Set.mem_interₛ.mpr
Proof state after:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ ∀ (t_1 : Set Form), t_1 ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p } → #x ∈ t_1
Theorem: theoryValuationBounding
Proof state before:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
⊢ ∀ (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 : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
r : Set Form
h₂ : r ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ #x ∈ r
Theorem: theoryValuationBounding
Proof state before:
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
r : Set Form
h₂ : r ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ #x ∈ r
Tactic:
exact h₁ ⟨⟨r,h₂.right.right⟩,h₂.left⟩ h₂.right.left
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
⊢ ∀ {t : Th} {f : Form}, t⊨f ↔ f ∈ ↑t
Tactic:
intros t f
Proof state after:
t : Th
f : Form
⊢ t⊨f ↔ f ∈ ↑t
Theorem: canonicalSatisfaction
Proof state before:
t : Th
f : Form
⊢ t⊨f ↔ f ∈ ↑t
Tactic:
cases f
Proof state after:
case atom
t : Th
a✝ : ℕ
⊢ t⊨#a✝ ↔ #a✝ ∈ ↑t

case neg
t : Th
a✝ : Form
⊢ t⊨~a✝ ↔ ~a✝ ∈ ↑t

case and
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹&a✝ ↔ a✝¹&a✝ ∈ ↑t

case or
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹¦a✝ ↔ a✝¹¦a✝ ∈ ↑t

case impl
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹⊃a✝ ↔ a✝¹⊃a✝ ∈ ↑t
Theorem: canonicalSatisfaction
Proof state before:
case atom
t : Th
a✝ : ℕ
⊢ t⊨#a✝ ↔ #a✝ ∈ ↑t

case neg
t : Th
a✝ : Form
⊢ t⊨~a✝ ↔ ~a✝ ∈ ↑t

case and
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹&a✝ ↔ a✝¹&a✝ ∈ ↑t

case or
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹¦a✝ ↔ a✝¹¦a✝ ∈ ↑t

case impl
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹⊃a✝ ↔ a✝¹⊃a✝ ∈ ↑t
Tactic:
all_goals apply Iff.intro <;> intros h₁
Proof state after:
case atom.mp
t : Th
a✝ : ℕ
h₁ : t⊨#a✝
⊢ #a✝ ∈ ↑t

case atom.mpr
t : Th
a✝ : ℕ
h₁ : #a✝ ∈ ↑t
⊢ t⊨#a✝

case neg.mp
t : Th
a✝ : Form
h₁ : t⊨~a✝
⊢ ~a✝ ∈ ↑t

case neg.mpr
t : Th
a✝ : Form
h₁ : ~a✝ ∈ ↑t
⊢ t⊨~a✝

case and.mp
t : Th
a✝¹ a✝ : Form
h₁ : t⊨a✝¹&a✝
⊢ a✝¹&a✝ ∈ ↑t

case and.mpr
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹&a✝ ∈ ↑t
⊢ t⊨a✝¹&a✝

case or.mp
t : Th
a✝¹ a✝ : Form
h₁ : t⊨a✝¹¦a✝
⊢ a✝¹¦a✝ ∈ ↑t

case or.mpr
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹¦a✝ ∈ ↑t
⊢ t⊨a✝¹¦a✝

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:
case atom.mp => exact h₁
Proof state after:
no goals
Theorem: canonicalSatisfaction
Proof state before:
t : Th
a✝ : ℕ
h₁ : #a✝ ∈ ↑t
⊢ t⊨#a✝
Tactic:
case atom.mpr => 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:
case and.mp f g => 
    have l₁ : f ∈ t := canonicalSatisfaction.mp h₁.left
    have l₂ : g ∈ t := canonicalSatisfaction.mp h₁.right
    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:
case and.mpr f g =>
    have l₁ : t ⊨ f := canonicalSatisfaction.mpr $ t.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.andE₁⟩
    have l₂ : t ⊨ g := canonicalSatisfaction.mpr $ t.property.mpr ⟨BProof.mp (BProof.ax h₁) BTheorem.andE₂⟩
    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:
case or.mp f g =>
  rw [primeAnalysis]
  intros p h₂
  let pr : Pr := ⟨⟨p, h₂.right.right⟩,h₂.left⟩
  have l₁ := @h₁ pr h₂.right.left
  cases l₁
  case inl h₃ => 
    have l₂ := canonicalSatisfaction.mp h₃
    exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₁⟩
  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